Merge PR #13553: Document Number Notation for primitive integers

Reviewed-by: jfehrle

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 64deb692fd..4dbf3b150b 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1709,6 +1709,8 @@ Number notations
             * :n:`Number.uint -> option @qualid__type`
             * :n:`Z -> @qualid__type`
             * :n:`Z -> option @qualid__type`
+            * :n:`Int63.int -> @qualid__type`
+            * :n:`Int63.int -> option @qualid__type`
             * :n:`Number.number -> @qualid__type`
             * :n:`Number.number -> option @qualid__type`
 
@@ -1721,6 +1723,8 @@ Number notations
             * :n:`@qualid__type -> option Number.uint`
             * :n:`@qualid__type -> Z`
             * :n:`@qualid__type -> option Z`
+            * :n:`@qualid__type -> Int63.int`
+            * :n:`@qualid__type -> option Int63.int`
             * :n:`@qualid__type -> Number.number`
             * :n:`@qualid__type -> option Number.number`
 
@@ -1825,6 +1829,13 @@ Number notations
      only for integers or non-negative integers, and the given number
      has a fractional or exponent part or is negative.
 
+   .. exn:: int63 are only non-negative numbers.
+
+      :n:`Int63.int` are unsigned integers.
+
+   .. exn:: overflow in int63 literal @bigint
+
+      The constant is too big to fit into an unsigned 63-bit integer :n:`Int63.int`.
 
    .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).