diff options
23 files changed, 264 insertions, 208 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 29a2b40162..dfa2aaf8ff 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -113,7 +113,7 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part - and exponent, optionally preceded by a minus sign. Hexadecimal numerals + and exponent, optionally preceded by a minus sign. Hexadecimal numbers 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 diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 06018304ab..f982898335 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1571,32 +1571,32 @@ Number notations parsing and printing functions, respectively. The parsing function :n:`@qualid__parse` should have one of the following types: - * :n:`Numeral.int -> @qualid__type` - * :n:`Numeral.int -> option @qualid__type` - * :n:`Numeral.uint -> @qualid__type` - * :n:`Numeral.uint -> option @qualid__type` + * :n:`Number.int -> @qualid__type` + * :n:`Number.int -> option @qualid__type` + * :n:`Number.uint -> @qualid__type` + * :n:`Number.uint -> option @qualid__type` * :n:`Z -> @qualid__type` * :n:`Z -> option @qualid__type` - * :n:`Numeral.numeral -> @qualid__type` - * :n:`Numeral.numeral -> option @qualid__type` + * :n:`Number.number -> @qualid__type` + * :n:`Number.number -> option @qualid__type` And the printing function :n:`@qualid__print` should have one of the following types: - * :n:`@qualid__type -> Numeral.int` - * :n:`@qualid__type -> option Numeral.int` - * :n:`@qualid__type -> Numeral.uint` - * :n:`@qualid__type -> option Numeral.uint` + * :n:`@qualid__type -> Number.int` + * :n:`@qualid__type -> option Number.int` + * :n:`@qualid__type -> Number.uint` + * :n:`@qualid__type -> option Number.uint` * :n:`@qualid__type -> Z` * :n:`@qualid__type -> option Z` - * :n:`@qualid__type -> Numeral.numeral` - * :n:`@qualid__type -> option Numeral.numeral` + * :n:`@qualid__type -> Number.number` + * :n:`@qualid__type -> option Number.number` .. deprecated:: 8.12 - Numeral notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by numeral - notations on :g:`Numeral.uint`, :g:`Numeral.int` and - :g:`Numeral.numeral`. + Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and + :g:`Decimal.decimal` are replaced respectively by number + notations on :g:`Number.uint`, :g:`Number.int` and + :g:`Number.number`. When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes @@ -1620,7 +1620,7 @@ Number notations returns :n:`(@qualid__parse m)` when parsing a literal :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a - :g:`Numeral.int`, :g:`Numeral.uint`, :g:`Z` or :g:`Numeral.numeral`, depending on the + :g:`Number.int`, :g:`Number.uint`, :g:`Z` or :g:`Number.number`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a @@ -1644,31 +1644,31 @@ Number notations .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support + The number notation registered for :token:`type` does not support the given number. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. - .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. 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). The parsing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. exn:: @qualid__print should go from @type to Number.int or (option Number.int). 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). The printing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a number notation. Parsing functions must always return ground terms, made up of applications of constructors, inductive types, and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a number notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a @@ -1741,16 +1741,16 @@ String notations concrete string expressed as a decimal. They may not return opaque constants. -The following errors apply to both string and numeral notations: +The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. - String and numeral notations can only be declared for inductive types with no + String and number notations can only be declared for inductive types with no arguments. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. - The inductive type used to register the string or numeral notation is no + The inductive type used to register the string or number notation is no longer available in the environment. Most likely, this is because the notation was declared inside a functor for an inductive type inside the functor. This use case is not currently diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 4d2972ef8f..e4f0967794 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,3 +1,4 @@ +theories/Init/Numeral.v theories/btauto/Algebra.v theories/btauto/Btauto.v theories/btauto/Reflect.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7c1328916b..e42066d2ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -22,7 +22,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Nat.v theories/Init/Decimal.v theories/Init/Hexadecimal.v - theories/Init/Numeral.v + theories/Init/Number.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 2db76719b8..fbf43be91f 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -64,7 +64,7 @@ let locate_numeral () = let hex = "num.hexadecimal.type" in let int = "num.num_int.type" in let uint = "num.num_uint.type" in - let num = "num.numeral.type" in + let num = "num.number.type" in if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 6dadd8c7fe..84913abcdc 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -124,7 +124,7 @@ Check r 2 3. End I. Require Import Coq.Numbers.Cyclic.Int63.Int63. -Module NumeralNotations. +Module NumberNotations. Module Test17. (** Test int63 *) Declare Scope test17_scope. @@ -134,7 +134,7 @@ Module NumeralNotations. Number Notation myint63 of_int to_int : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. -End NumeralNotations. +End NumberNotations. Module K. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 8065c8d311..b00fd3b485 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -1,9 +1,9 @@ The command has indeed failed with message: -Unexpected term (nat -> nat) while parsing a numeral notation. +Unexpected term (nat -> nat) while parsing a number notation. The command has indeed failed with message: -Unexpected non-option term opaque4 while parsing a numeral notation. +Unexpected non-option term opaque4 while parsing a number notation. The command has indeed failed with message: -Unexpected term (fun (A : Type) (x : A) => x) while parsing a numeral +Unexpected term (fun (A : Type) (x : A) => x) while parsing a number notation. let v := 0%ppp in v : punit : punit @@ -32,7 +32,7 @@ Warning: To avoid stack overflow, large numbers in punit are interpreted as applications of pto_punits. [abstract-large-number,numbers] The command has indeed failed with message: In environment -v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit +v := pto_punits (Number.UIntDec (Decimal.D1 Decimal.Nil)) : punit The term "v" has type "punit@{Set}" while it is expected to have type "punit@{u}". S @@ -61,7 +61,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". - = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} + = {| unwrap := Number.UIntDec (Decimal.D0 Decimal.Nil) |} : wuint let v := 0%wuint8' in v : wuint : wuint @@ -82,7 +82,7 @@ function (of_uint) targets an option type. The command has indeed failed with message: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] -let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit +let v := of_uint (Number.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit : unit let v := 0%test13 in v : unit : unit diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v index e411005da3..af0aa895d1 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -5,17 +5,17 @@ Declare Scope opaque_scope. (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) Module Test1. Axiom hold : forall {A B C}, A -> B -> C. - Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Number Notation Numeral.int opaque3 opaque3 : opaque_scope. + Definition opaque3 (x : Number.int) : Number.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Number Notation Number.int opaque3 opaque3 : opaque_scope. Delimit Scope opaque_scope with opaque. Fail Check 1%opaque. End Test1. (* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) Module Test2. - Axiom opaque4 : option Numeral.int. - Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. - Number Notation Numeral.int opaque6 opaque6 : opaque_scope. + Axiom opaque4 : option Number.int. + Definition opaque6 (x : Number.int) : option Number.int := opaque4. + Number Notation Number.int opaque6 opaque6 : opaque_scope. Delimit Scope opaque_scope with opaque. Open Scope opaque_scope. Fail Check 1%opaque. @@ -24,8 +24,8 @@ End Test2. Declare Scope silly_scope. Module Test3. - Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). - Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). + Inductive silly := SILLY (v : Number.uint) (f : forall A, A -> A). + Definition to_silly (v : Number.uint) := SILLY v (fun _ x => x). Definition of_silly (v : silly) := match v with SILLY v _ => v end. Number Notation silly to_silly of_silly : silly_scope. Delimit Scope silly_scope with silly. @@ -45,15 +45,15 @@ Module Test4. Declare Scope upp. Declare Scope ppps. Polymorphic NonCumulative Inductive punit := ptt. - Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. - Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. - Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. - Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. - Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Number.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Number.uint := Nat.to_num_uint 0. + Definition to_punit (v : Number.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Number.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Number.uint := Nat.to_num_uint 0. + Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0. Number Notation punit to_punit of_punit : pto. Number Notation punit pto_punit of_punit : ppo. Number Notation punit to_punit pof_punit : ptp. @@ -96,7 +96,7 @@ Module Test5. End Test5. Module Test6. - (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Check that number notations on enormous terms don't take forever to print/parse *) (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) Fixpoint ack (n m : nat) : nat := match n with @@ -113,8 +113,8 @@ Module Test6. Local Set Primitive Projections. Record > wnat := wrap { unwrap :> nat }. - Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x. - Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. + Definition to_uint (x : wnat) : Number.uint := Nat.to_num_uint x. + Definition of_uint (x : Number.uint) : wnat := Nat.of_num_uint x. Module Export Scopes. Declare Scope wnat_scope. Delimit Scope wnat_scope with wnat. @@ -138,7 +138,7 @@ End Test6_2. Module Test7. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Declare Scope wuint_scope. Delimit Scope wuint_scope with wuint. Number Notation wuint wrap unwrap : wuint_scope. @@ -148,7 +148,7 @@ End Test7. Module Test8. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Declare Scope wuint8_scope. Declare Scope wuint8'_scope. Delimit Scope wuint8_scope with wuint8. @@ -177,7 +177,7 @@ Module Test9. Delimit Scope wuint9'_scope with wuint9'. Section with_let. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Numeral.uint }. + Record wuint := wrap { unwrap : Number.uint }. Let wrap' := wrap. Let unwrap' := unwrap. Local Notation wrap'' := wrap. @@ -194,8 +194,8 @@ End Test9. Module Test10. (* Test that it is only a warning to add abstract after to an optional parsing function *) Definition to_uint (v : unit) := Nat.to_num_uint 0. - Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. - Definition of_any_uint (v : Numeral.uint) := tt. + Definition of_uint (v : Number.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Number.uint) := tt. Declare Scope unit_scope. Declare Scope unit2_scope. Delimit Scope unit_scope with unit. @@ -209,11 +209,11 @@ Module Test10. End Test10. Module Test12. - (* Test for numeral notations on context variables *) + (* Test for number notations on context variables *) Declare Scope test12_scope. Delimit Scope test12_scope with test12. Section test12. - Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). + Context (to_uint : unit -> Number.uint) (of_uint : Number.uint -> unit). Number Notation unit of_uint to_uint : test12_scope. Check let v := 1%test12 in v : unit. @@ -221,15 +221,15 @@ Module Test12. End Test12. Module Test13. - (* Test for numeral notations on notations which do not denote references *) + (* Test for number notations on notations which do not denote references *) Declare Scope test13_scope. Declare Scope test13'_scope. Declare Scope test13''_scope. Delimit Scope test13_scope with test13. Delimit Scope test13'_scope with test13'. Delimit Scope test13''_scope with test13''. - Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x y : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Definition to_uint_good := to_uint tt. Notation to_uint' := (to_uint tt). Notation to_uint'' := (to_uint _). @@ -242,7 +242,7 @@ Module Test13. End Test13. Module Test14. - (* Test that numeral notations follow [Import], not [Require], and + (* Test that number notations follow [Import], not [Require], and also test that [Local Number Notation]s do not escape modules nor sections. *) Declare Scope test14_scope. @@ -254,8 +254,8 @@ Module Test14. Delimit Scope test14''_scope with test14''. Delimit Scope test14'''_scope with test14'''. Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Local Number Notation unit of_uint to_uint : test14_scope. Global Number Notation unit of_uint to_uint : test14'_scope. Check let v := 0%test14 in v : unit. @@ -267,8 +267,8 @@ Module Test14. Fail Check let v := 0%test14 in v : unit. Check let v := 0%test14' in v : unit. Section InnerSection. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Local Number Notation unit of_uint to_uint : test14''_scope. Fail Global Number Notation unit of_uint to_uint : test14'''_scope. Check let v := 0%test14'' in v : unit. @@ -283,8 +283,8 @@ Module Test15. Declare Scope test15_scope. Delimit Scope test15_scope with test15. Module Inner. - Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : unit := tt. + Definition to_uint (x : unit) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : unit := tt. Number Notation unit of_uint to_uint : test15_scope. Check let v := 0%test15 in v : unit. End Inner. @@ -306,8 +306,8 @@ Module Test16. End A. Module F (a : A). Inductive Foo := foo (_ : a.T). - Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. - Definition of_uint (x : Numeral.uint) : Foo := foo a.t. + Definition to_uint (x : Foo) : Number.uint := Nat.to_num_uint O. + Definition of_uint (x : Number.uint) : Foo := foo a.t. Global Number Notation Foo of_uint to_uint : test16_scope. Check let v := 0%test16 in v : Foo. End F. @@ -352,8 +352,8 @@ Module Test18. Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. Definition nat_of_Q (x : Q) : option nat := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. - Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). - Definition uint_of_Q (x : Q) : option Numeral.uint + Definition Q_of_uint (x : Number.uint) : Q := Q_of_nat (Nat.of_num_uint x). + Definition uint_of_Q (x : Q) : option Number.uint := option_map Nat.to_num_uint (nat_of_Q x). Number Notation Q Q_of_uint uint_of_Q : Q_scope. @@ -411,7 +411,7 @@ Module Test20. Record > ty := { t : Type ; kt : known_type t }. - Definition ty_of_uint (x : Numeral.uint) : option ty + Definition ty_of_uint (x : Number.uint) : option ty := match Nat.of_num_uint x with | 0 => @Some ty zero | 1 => @Some ty one @@ -421,7 +421,7 @@ Module Test20. | 5 => @Some ty type | _ => None end. - Definition uint_of_ty (x : ty) : Numeral.uint + Definition uint_of_ty (x : ty) : Number.uint := Nat.to_num_uint match kt x with | prop => 3 | set => 4 diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 09feca71e7..914e7f88c6 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -30,15 +30,15 @@ implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool BoolSpec: Prop -> Prop -> bool -> Prop -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool +Number.number_beq: Number.number -> Number.number -> bool Nat.eqb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool @@ -64,34 +64,34 @@ eq_true_rec: bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b eq_true_sind: forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true Hexadecimal.internal_int_dec_lb0: forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true Decimal.internal_decimal_dec_lb: forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true Hexadecimal.internal_int_dec_bl0: forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_bl: forall x y : Hexadecimal.hexadecimal, Hexadecimal.hexadecimal_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true Decimal.internal_int_dec_bl: forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y Decimal.internal_int_dec_lb: forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y Byte.of_bits: bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> Byte.byte @@ -160,21 +160,21 @@ f_equal2_mult: f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Decimal.internal_decimal_dec_lb: forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true Hexadecimal.internal_hexadecimal_dec_bl: @@ -213,18 +213,18 @@ bool_choice: forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_lb: forall x y : Hexadecimal.hexadecimal, x = y -> Hexadecimal.hexadecimal_beq x y = true @@ -306,12 +306,12 @@ nat_rect_plus: (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) (fun _ : nat => f) n Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Numeral.internal_numeral_dec_bl: - forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y -Numeral.internal_int_dec_bl1: - forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y -Numeral.internal_uint_dec_bl1: - forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Number.internal_number_dec_bl: + forall x y : Number.number, Number.number_beq x y = true -> x = y +Number.internal_int_dec_bl1: + forall x y : Number.int, Number.int_beq x y = true -> x = y +Number.internal_uint_dec_bl1: + forall x y : Number.uint, Number.uint_beq x y = true -> x = y Hexadecimal.internal_hexadecimal_dec_bl: forall x y : Hexadecimal.hexadecimal, Hexadecimal.hexadecimal_beq x y = true -> x = y @@ -328,12 +328,12 @@ Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), Byte.to_bits (Byte.of_bits b) = b -Numeral.internal_numeral_dec_lb: - forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true -Numeral.internal_uint_dec_lb1: - forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true -Numeral.internal_int_dec_lb1: - forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true +Number.internal_number_dec_lb: + forall x y : Number.number, x = y -> Number.number_beq x y = true +Number.internal_uint_dec_lb1: + forall x y : Number.uint, x = y -> Number.uint_beq x y = true +Number.internal_int_dec_lb1: + forall x y : Number.int, x = y -> Number.int_beq x y = true Decimal.internal_int_dec_lb: forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true Hexadecimal.internal_hexadecimal_dec_lb: @@ -391,7 +391,7 @@ Nat.lor: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.of_hex_uint: Hexadecimal.uint -> nat Nat.of_uint: Decimal.uint -> nat -Nat.of_num_uint: Numeral.uint -> nat +Nat.of_num_uint: Number.uint -> nat length: forall [A : Type], list A -> nat plus_n_O: forall n : nat, n = n + 0 plus_O_n: forall n : nat, 0 + n = n diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 9554581ebe..2f0d854ac6 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -21,15 +21,15 @@ orb: bool -> bool -> bool implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.number_beq: Number.number -> Number.number -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 80b03e8a0b..d705ec898b 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -7,15 +7,15 @@ orb: bool -> bool -> bool implb: bool -> bool -> bool Nat.odd: nat -> bool Nat.even: nat -> bool -Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Number.uint_beq: Number.uint -> Number.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool Hexadecimal.hexadecimal_beq: Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool -Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool -Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Number.number_beq: Number.number -> Number.number -> bool +Number.int_beq: Number.int -> Number.int -> bool Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool @@ -50,7 +50,7 @@ Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat Hexadecimal.nb_digits: Hexadecimal.uint -> nat Nat.of_hex_uint: Hexadecimal.uint -> nat -Nat.of_num_uint: Numeral.uint -> nat +Nat.of_num_uint: Number.uint -> nat Nat.of_uint: Decimal.uint -> nat Decimal.nb_digits: Decimal.uint -> nat Nat.tail_addmul: nat -> nat -> nat -> nat diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index 7b2bb00ce0..219d953c97 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -18,7 +18,7 @@ Require Import Arith. Check (0 + Z.of_nat 11)%Z. (* Check hexadecimal printing *) -Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). +Definition to_num_int n := Number.IntHex (Z.to_hex_int n). Number Notation Z Z.of_num_int to_num_int : Z_scope. Check 42%Z. Check (-42)%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 437b4a68e9..a7366f2d35 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -2,10 +2,10 @@ Declare Scope A. Declare Scope B. Delimit Scope A with A. Delimit Scope B with B. -Definition to_unit (v : Numeral.uint) : option unit +Definition to_unit (v : Number.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. -Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. -Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. +Definition of_unit (v : unit) : Number.uint := Nat.to_num_uint 0. +Definition of_unit' (v : unit) : Number.uint := Nat.to_num_uint 1. Number Notation unit to_unit of_unit : A. Number Notation unit to_unit of_unit' : B. Definition f x : unit := x. diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumberNotationsNoLocal.v index fe97f10ddf..e19d06cfa7 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumberNotationsNoLocal.v @@ -1,4 +1,4 @@ -(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) +(* Test that number notations don't work on proof-local variables, especially not ones containing evars *) Inductive unit11 := tt11. Declare Scope unit11_scope. Delimit Scope unit11_scope with unit11. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 7c8cf0b536..bc48311151 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import Notations Logic Datatypes. -Require Decimal Hexadecimal Numeral. +Require Decimal Hexadecimal Number. Local Open Scope nat_scope. (**********************************************************************) @@ -212,10 +212,10 @@ Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) := Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O. -Definition of_num_uint (d:Numeral.uint) := +Definition of_num_uint (d:Number.uint) := match d with - | Numeral.UIntDec d => of_uint d - | Numeral.UIntHex d => of_hex_uint d + | Number.UIntDec d => of_uint d + | Number.UIntHex d => of_hex_uint d end. Fixpoint to_little_uint n acc := @@ -236,9 +236,9 @@ Fixpoint to_little_hex_uint n acc := Definition to_hex_uint n := Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero). -Definition to_num_uint n := Numeral.UIntDec (to_uint n). +Definition to_num_uint n := Number.UIntDec (to_uint n). -Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n). +Definition to_num_hex_uint n := Number.UIntHex (to_hex_uint n). Definition of_int (d:Decimal.int) : option nat := match Decimal.norm d with @@ -252,17 +252,17 @@ Definition of_hex_int (d:Hexadecimal.int) : option nat := | _ => None end. -Definition of_num_int (d:Numeral.int) : option nat := +Definition of_num_int (d:Number.int) : option nat := match d with - | Numeral.IntDec d => of_int d - | Numeral.IntHex d => of_hex_int d + | Number.IntDec d => of_int d + | Number.IntHex d => of_hex_int d end. Definition to_int n := Decimal.Pos (to_uint n). Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). -Definition to_num_int n := Numeral.IntDec (to_int n). +Definition to_num_int n := Number.IntDec (to_int n). (** ** Euclidean division *) diff --git a/theories/Init/Number.v b/theories/Init/Number.v new file mode 100644 index 0000000000..228f84b179 --- /dev/null +++ b/theories/Init/Number.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Decimal or Hexadecimal numbers *) + +Require Import Decimal Hexadecimal. + +Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint). + +Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int). + +Variant number := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal). + +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for number. + +Register uint as num.num_uint.type. +Register int as num.num_int.type. +Register number as num.number.type. + +(** Pseudo-conversion functions used when declaring + Number Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v index 179547d0b3..c87f17ee5a 100644 --- a/theories/Init/Numeral.v +++ b/theories/Init/Numeral.v @@ -8,26 +8,47 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** * Decimal or Hexadecimal numbers *) - -Require Import Decimal Hexadecimal. - -Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint). - -Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int). - -Variant numeral := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal). - -Scheme Equality for uint. -Scheme Equality for int. -Scheme Equality for numeral. - -Register uint as num.num_uint.type. -Register int as num.num_int.type. -Register numeral as num.numeral.type. - -(** Pseudo-conversion functions used when declaring - Number Notations on [uint] and [int]. *) - -Definition uint_of_uint (i:uint) := i. -Definition int_of_int (i:int) := i. +(** * Deprecated: use Number.v instead *) + +Require Import Decimal Hexadecimal Number. + +#[deprecated(since="8.13",note="Use Number.uint instead.")] +Notation uint := uint (only parsing). +#[deprecated(since="8.13",note="Use Number.UintDec instead.")] +Notation UIntDec := UIntDec (only parsing). +#[deprecated(since="8.13",note="Use Number.UintHex instead.")] +Notation UIntHex := UIntHex (only parsing). + +#[deprecated(since="8.13",note="Use Number.int instead.")] +Notation int := int (only parsing). +#[deprecated(since="8.13",note="Use Number.IntDec instead.")] +Notation IntDec := IntDec (only parsing). +#[deprecated(since="8.13",note="Use Number.IntHex instead.")] +Notation IntHex := IntHex (only parsing). + +#[deprecated(since="8.13",note="Use Number.numeral instead.")] +Notation numeral := number (only parsing). +#[deprecated(since="8.13",note="Use Number.Dec instead.")] +Notation Dec := Dec (only parsing). +#[deprecated(since="8.13",note="Use Number.Hex instead.")] +Notation Hex := Hex (only parsing). + +#[deprecated(since="8.13",note="Use Number.uint_beq instead.")] +Notation uint_beq := uint_beq (only parsing). +#[deprecated(since="8.13",note="Use Number.uint_eq_dec instead.")] +Notation uint_eq_dec := uint_eq_dec (only parsing). +#[deprecated(since="8.13",note="Use Number.int_beq instead.")] +Notation int_beq := int_beq (only parsing). +#[deprecated(since="8.13",note="Use Number.int_eq_dec instead.")] +Notation int_eq_dec := int_eq_dec (only parsing). +#[deprecated(since="8.13",note="Use Number.numeral_beq instead.")] +Notation numeral_beq := number_beq (only parsing). +#[deprecated(since="8.13",note="Use Number.numeral_eq_dec instead.")] +Notation numeral_eq_dec := number_eq_dec (only parsing). + +Register number as num.numeral.type. + +#[deprecated(since="8.13",note="Use Number.uint_of_uint instead.")] +Notation uint_of_uint := uint_of_uint (only parsing). +#[deprecated(since="8.13",note="Use Number.int_of_int instead.")] +Notation int_of_int := int_of_int (only parsing). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 0fe3d5491e..141864d257 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -17,6 +17,7 @@ Require Coq.Init.Byte. Require Coq.Init.Decimal. Require Coq.Init.Hexadecimal. Require Coq.Init.Numeral. +Require Coq.Init.Number. Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. @@ -35,17 +36,17 @@ Declare ML Module "string_notation_plugin". (* Parsing / printing of hexadecimal numbers *) Arguments Nat.of_hex_uint d%hex_uint_scope. Arguments Nat.of_hex_int d%hex_int_scope. -Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint : hex_uint_scope. -Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Number.int Number.int_of_int Number.int_of_int : hex_int_scope. (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. Arguments Nat.of_int d%dec_int_scope. -Number Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint +Number Notation Number.uint Number.uint_of_uint Number.uint_of_uint : dec_uint_scope. -Number Notation Numeral.int Numeral.int_of_int Numeral.int_of_int +Number Notation Number.int Number.int_of_int Number.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 222e76c3e7..4142bb786f 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -390,10 +390,10 @@ Definition of_uint (d:Decimal.uint) := Pos.of_uint d. Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d. -Definition of_num_uint (d:Numeral.uint) := +Definition of_num_uint (d:Number.uint) := match d with - | Numeral.UIntDec d => of_uint d - | Numeral.UIntHex d => of_hex_uint d + | Number.UIntDec d => of_uint d + | Number.UIntHex d => of_hex_uint d end. Definition of_int (d:Decimal.int) := @@ -408,10 +408,10 @@ Definition of_hex_int (d:Hexadecimal.int) := | Hexadecimal.Neg _ => None end. -Definition of_num_int (d:Numeral.int) := +Definition of_num_int (d:Number.int) := match d with - | Numeral.IntDec d => of_int d - | Numeral.IntHex d => of_hex_int d + | Number.IntDec d => of_int d + | Number.IntHex d => of_hex_int d end. Definition to_uint n := @@ -426,13 +426,13 @@ Definition to_hex_uint n := | pos p => Pos.to_hex_uint p end. -Definition to_num_uint n := Numeral.UIntDec (to_uint n). +Definition to_num_uint n := Number.UIntDec (to_uint n). Definition to_int n := Decimal.Pos (to_uint n). Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). -Definition to_num_int n := Numeral.IntDec (to_int n). +Definition to_num_int n := Number.IntDec (to_int n). Number Notation N of_num_uint to_num_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 7c846571a7..c203c178f5 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -17,7 +17,7 @@ the [Decimal.int] representation. When working with numbers with thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your - development, this file provides some alternative [Numeral + development, this file provides some alternative [Number Notation] commands that use [Z] as bridge type. To enable these commands, just be sure to [Require] this file after other files defining numeral notations. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index b41cd571dc..958778762d 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -639,10 +639,10 @@ Fixpoint of_hex_uint (d:Hexadecimal.uint) : N := | Hexadecimal.Df l => Npos (of_hex_uint_acc l 1~1~1~1) end. -Definition of_num_uint (d:Numeral.uint) : N := +Definition of_num_uint (d:Number.uint) : N := match d with - | Numeral.UIntDec d => of_uint d - | Numeral.UIntHex d => of_hex_uint d + | Number.UIntDec d => of_uint d + | Number.UIntHex d => of_hex_uint d end. Definition of_int (d:Decimal.int) : option positive := @@ -665,10 +665,10 @@ Definition of_hex_int (d:Hexadecimal.int) : option positive := | Hexadecimal.Neg _ => None end. -Definition of_num_int (d:Numeral.int) : option positive := +Definition of_num_int (d:Number.int) : option positive := match d with - | Numeral.IntDec d => of_int d - | Numeral.IntHex d => of_hex_int d + | Number.IntDec d => of_int d + | Number.IntHex d => of_hex_int d end. Fixpoint to_little_uint p := @@ -689,13 +689,13 @@ Fixpoint to_little_hex_uint p := Definition to_hex_uint p := Hexadecimal.rev (to_little_hex_uint p). -Definition to_num_uint p := Numeral.UIntDec (to_uint p). +Definition to_num_uint p := Number.UIntDec (to_uint p). Definition to_int n := Decimal.Pos (to_uint n). Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p). -Definition to_num_int n := Numeral.IntDec (to_int n). +Definition to_num_int n := Number.IntDec (to_int n). Number Notation positive of_num_int to_num_uint : positive_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 192dcd885b..151355519e 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -117,16 +117,16 @@ Definition to_hexadecimal (q:Q) : option Hexadecimal.hexadecimal := | _ => None end. -Definition of_numeral (d:Numeral.numeral) : option Q := +Definition of_numeral (d:Number.number) : option Q := match d with - | Numeral.Dec d => Some (of_decimal d) - | Numeral.Hex d => Some (of_hexadecimal d) + | Number.Dec d => Some (of_decimal d) + | Number.Hex d => Some (of_hexadecimal d) end. -Definition to_numeral (q:Q) : option Numeral.numeral := +Definition to_numeral (q:Q) : option Number.number := match to_decimal q with | None => None - | Some q => Some (Numeral.Dec q) + | Some q => Some (Number.Dec q) end. Number Notation Q of_numeral to_numeral : Q_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 69ed101f24..9415903fa4 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -311,10 +311,10 @@ Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d). Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d). -Definition of_num_uint (d:Numeral.uint) := +Definition of_num_uint (d:Number.uint) := match d with - | Numeral.UIntDec d => of_uint d - | Numeral.UIntHex d => of_hex_uint d + | Number.UIntDec d => of_uint d + | Number.UIntHex d => of_hex_uint d end. Definition of_int (d:Decimal.int) := @@ -329,10 +329,10 @@ Definition of_hex_int (d:Hexadecimal.int) := | Hexadecimal.Neg d => opp (of_hex_uint d) end. -Definition of_num_int (d:Numeral.int) := +Definition of_num_int (d:Number.int) := match d with - | Numeral.IntDec d => of_int d - | Numeral.IntHex d => of_hex_int d + | Number.IntDec d => of_int d + | Number.IntHex d => of_hex_int d end. Definition to_int n := @@ -349,7 +349,7 @@ Definition to_hex_int n := | neg p => Hexadecimal.Neg (Pos.to_hex_uint p) end. -Definition to_num_int n := Numeral.IntDec (to_int n). +Definition to_num_int n := Number.IntDec (to_int n). (** ** Iteration of a function |