diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 60cd4c4ad8..955f2055e4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1429,10 +1429,31 @@ Abbreviations Notation F p P := (force2 p (fun p => P)). Check exists x y, F (x,y) (x >= 1 /\ y >= 2). +.. extracted from Gallina chapter + +Numerals and strings +-------------------- + +.. insertprodn primitive_notations primitive_notations + +.. prodn:: + primitive_notations ::= @numeral + | @string + +Numerals and strings have no predefined semantics in the calculus. They are +merely notations that can be bound to objects through the notation mechanism. +Initially, numerals are bound to Peano’s representation of natural +numbers (see :ref:`datatypes`). + +.. note:: + + Negative integers are not at the same level as :n:`@num`, for this + would make precedence unnatural. + .. _numeral-notations: Numeral notations ------------------ +~~~~~~~~~~~~~~~~~ .. cmd:: Numeral Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } :name: Numeral Notation @@ -1557,7 +1578,7 @@ Numeral notations opaque constants. String notations ------------------ +~~~~~~~~~~~~~~~~ .. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name :name: String Notation |