diff options
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 609884ce1d..03571ad680 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1741,6 +1741,12 @@ Number notations sorts, primitive integers, primitive floats, primitive arrays and type constants for primitive types) will be considered for printing. + .. note:: + For example, :n:`@qualid__type` can be :n:`PrimInt63.int`, + in which case :n:`@qualid__print` takes :n:`PrimInt63.int_wrapper` as input + instead of :n:`PrimInt63.int`. See below for an + :ref:`example <example-number-notation-primitive-int>`. + .. _number-string-via: :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` @@ -2066,6 +2072,23 @@ The following errors apply to both string and number notations: Check 3. +.. _example-number-notation-primitive-int: + +.. example:: Number Notation for primitive integers + + This shows the use of the primitive + integers :n:`PrimInt63.int` as :n:`@qualid__type`. It is the way + parsing and printing of primitive integers are actually implemented + in `PrimInt63.v`. + + .. coqtop:: in reset + + Require Import Int63. + Definition parser (x : pos_neg_int63) : option int := + match x with Pos p => Some p | Neg _ => None end. + Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). + Number Notation int parser printer : int63_scope. + .. _example-number-notation-non-inductive: .. example:: Number Notation for a non inductive type |