From 46b9480a717d5ca78e354fa843f39eed87cb7b15 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:08:00 +0200 Subject: [refman] Rename num to natural --- doc/sphinx/language/core/basic.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 1f0d696d99..63c4243921 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -115,20 +115,20 @@ Numerals Numerals are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@num` is a non-negative + a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn numeral hexdigit .. prodn:: - numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum } - | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum } - int ::= {? - } @num - num ::= {| @decnum | @hexnum } - decnum ::= @digit {* {| @digit | _ } } + numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } + int ::= {? - } @natural + natural ::= {| @decnat | @hexnat } + decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 - hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } + hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } .. todo PR need some code fixes for hex, see PR 11948 @@ -292,7 +292,7 @@ rest of the |Coq| manual: :term:`terms ` and :term:`types .. prodn:: document ::= {* @sentence } sentence ::= {? @attributes } @command . - | {? @attributes } {? @num : } @query_command . + | {? @attributes } {? @natural : } @query_command . | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... } | @control_command -- cgit v1.2.3 From 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:09:00 +0200 Subject: [refman] Rename numeral to number --- doc/sphinx/language/core/basic.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 63c4243921..be513833ad 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -119,10 +119,10 @@ Numerals integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. - .. insertprodn numeral hexdigit + .. insertprodn number hexdigit .. prodn:: - numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } int ::= {? - } @natural natural ::= {| @decnat | @hexnat } -- cgit v1.2.3 From 724966f56caa66a5ddc9a992cf870ebc2efae004 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 11:53:49 +0200 Subject: [refman] Rename int to integer --- doc/sphinx/language/core/basic.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index be513833ad..d248839fa0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -111,11 +111,11 @@ Identifiers symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. -Numerals - Numerals are sequences of digits with an optional fractional part +Numbers + Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative + a number without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. @@ -124,7 +124,7 @@ Numerals .. prodn:: number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } - int ::= {? - } @natural + integer ::= {? - } @natural natural ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 @@ -434,7 +434,7 @@ gray boxes after the labels "Flag", "Option" and "Table". In the pdf, they appear after a boldface label. They are listed in the :ref:`options_index`. -.. cmd:: Set @setting_name {? {| @int | @string } } +.. cmd:: Set @setting_name {? {| @integer | @string } } :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag -- cgit v1.2.3 From 031cc2ba1a19a06766df85b8693c72f16fa62de6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 12:07:23 +0200 Subject: [refman] Explicit integer and natural As respectively bigint and bignat that fit into an OCaml int. --- doc/sphinx/language/core/basic.rst | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index d248839fa0..9308da6d27 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -114,9 +114,9 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals - start with ``0x`` or ``0X``. :n:`@int` is an integer; - a number without fractional nor exponent parts. :n:`@natural` is a non-negative - integer. Underscores embedded in the digits are ignored, for example + start with ``0x`` or ``0X``. :n:`@bigint` are integers; + numbers without fractional nor exponent parts. :n:`@bignat` are non-negative + integers. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn number hexdigit @@ -125,13 +125,17 @@ Numbers number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } integer ::= {? - } @natural - natural ::= {| @decnat | @hexnat } + natural ::= @bignat + bigint ::= {? - } @bignat + bignat ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } - .. todo PR need some code fixes for hex, see PR 11948 + :n:`@integer` and :n:`@natural` are limited to the range that fits + into an OCaml integer (63-bit integers on most architectures). + :n:`@bigint` and :n:`@bignat` have no range limitation. Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent -- cgit v1.2.3 From ad7140a7127b147caf20d7c3803b918e3c6776f5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:29:00 +0200 Subject: [numeral notation] Improve documentation Following reviews from Jim Fehrle on #12218 and #12979 --- doc/sphinx/language/core/basic.rst | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9308da6d27..45bdc019ac 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -137,11 +137,20 @@ Numbers into an OCaml integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. + The :ref:`standard library ` provides some + :ref:`interpretations ` for :n:`@number`. The + :cmd:`Number Notation` mechanism offers the user + a way to define custom parsers and printers for :n:`@number`. + Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent a double quote character within a string. In the grammar, strings are identified with :production:`string`. + The :cmd:`String Notation` mechanism offers the + user a way to define custom parsers and printers for + :token:`string`. + Keywords The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the `-noinit` -- cgit v1.2.3