diff options
| author | Théo Zimmermann | 2020-05-14 11:45:16 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 12:39:36 +0200 |
| commit | 95c4fc791b1eda5357855f706dfdb4c050d6c28e (patch) | |
| tree | df2e9f3316514b01f2f84a53f5ea882d310c1188 /doc/sphinx/user-extensions | |
| parent | 6a9486eaa9a0de2af2f518cef09db7ea9afa9ab1 (diff) | |
Reintroduce leftover parts; update index files; small fixes.
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ea5ad79a80..e49073f593 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1383,10 +1383,29 @@ Abbreviations exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments. +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 @@ -1504,7 +1523,7 @@ Numeral notations opaque constants. String notations ------------------ +~~~~~~~~~~~~~~~~ .. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name :name: String Notation |