diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e5eb7eb4f5..1e201953b3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1473,6 +1473,10 @@ Numeral notations :n:`@ident__2` to the number will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1618,6 +1622,10 @@ String notations :n:`@ident__2` to the string will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. exn:: Cannot interpret this string as a value of type @type The string notation registered for :token:`type` does not support |