aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Compat/Coq88.v14
-rw-r--r--theories/FSets/FSetAVL.v2
-rw-r--r--theories/FSets/FSetEqProperties.v4
-rw-r--r--theories/Init/Datatypes.v1
-rw-r--r--theories/Init/Decimal.v14
-rw-r--r--theories/Init/Nat.v4
-rw-r--r--theories/Init/Peano.v1
-rw-r--r--theories/Init/Prelude.v19
-rw-r--r--theories/MSets/MSetEqProperties.v4
-rw-r--r--theories/MSets/MSetGenTree.v2
-rw-r--r--theories/NArith/BinNat.v2
-rw-r--r--theories/NArith/BinNatDef.v9
-rw-r--r--theories/Numbers/AltBinNotations.v69
-rw-r--r--theories/Numbers/BinNums.v16
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v4
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v2
-rw-r--r--theories/Numbers/Integer/Abstract/ZBits.v6
-rw-r--r--theories/Numbers/Natural/Abstract/NBits.v6
-rw-r--r--theories/PArith/BinPos.v2
-rw-r--r--theories/PArith/BinPosDef.v13
-rw-r--r--theories/Reals/Rsqrt_def.v2
-rw-r--r--theories/Structures/GenericMinMax.v2
-rw-r--r--theories/ZArith/BinInt.v2
-rw-r--r--theories/ZArith/BinIntDef.v15
24 files changed, 175 insertions, 40 deletions
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 4142af05d2..578425bfb5 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,3 +9,17 @@
(************************************************************************)
(** Compatibility file for making Coq act similar to Coq v8.8 *)
+(** In Coq 8.9, prim token notations follow [Import] rather than
+ [Require]. So we make all of the relevant notations accessible in
+ compatibility mode. *)
+Require Coq.Strings.Ascii Coq.Strings.String.
+Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
+Require Coq.Reals.Rdefinitions.
+Require Coq.Numbers.Cyclic.Int31.Int31.
+Declare ML Module "string_syntax_plugin".
+Declare ML Module "ascii_syntax_plugin".
+Declare ML Module "r_syntax_plugin".
+Declare ML Module "int31_syntax_plugin".
+Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
+Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope.
+Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 3c9b6b428b..dcaea894eb 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -15,7 +15,7 @@
It follows the implementation from Ocaml's standard library,
All operations given here expect and produce well-balanced trees
- (in the ocaml sense: heigths of subtrees shouldn't differ by more
+ (in the ocaml sense: heights of subtrees shouldn't differ by more
than 2), and hence has low complexities (e.g. add is logarithmic
in the size of the set). But proving these balancing preservations
is in fact not necessary for ensuring correct operational behavior
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 56844f4773..59b2f789ab 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
auto with set.
Qed.
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
Lemma union_subset_1: subset s (union s s')=true.
Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
rewrite not_mem_iff; auto.
Qed.
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
Lemma inter_subset_1: subset (inter s s') s=true.
Proof.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 05b741f0ac..1e6843d511 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -12,7 +12,6 @@ Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
-Declare ML Module "nat_syntax_plugin".
(********************************************************************)
(** * Datatypes with zero and one element *)
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 57163b1b07..1ff00ec11c 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,10 +42,10 @@ Notation zero := (D0 Nil).
Inductive int := Pos (d:uint) | Neg (d:uint).
-Delimit Scope uint_scope with uint.
-Bind Scope uint_scope with uint.
-Delimit Scope int_scope with int.
-Bind Scope int_scope with int.
+Delimit Scope dec_uint_scope with uint.
+Bind Scope dec_uint_scope with uint.
+Delimit Scope dec_int_scope with int.
+Bind Scope dec_int_scope with int.
(** This representation favors simplicity over canonicity.
For normalizing numbers, we need to remove head zero digits,
@@ -161,3 +161,9 @@ with succ_double d :=
end.
End Little.
+
+(** Pseudo-conversion functions used when declaring
+ Numeral Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index ad1bc717c4..eb4ba0e5e6 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -24,6 +24,10 @@ Definition t := nat.
(** ** Constants *)
+Local Notation "0" := O.
+Local Notation "1" := (S O).
+Local Notation "2" := (S (S O)).
+
Definition zero := 0.
Definition one := 1.
Definition two := 2.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index d5322d0945..65e5e76a22 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -31,6 +31,7 @@ Require Import Logic.
Require Coq.Init.Nat.
Open Scope nat_scope.
+Local Notation "0" := O.
Definition eq_S := f_equal S.
Definition f_equal_nat := f_equal (A:=nat).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 802f18c0f2..6d98bcb34a 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,9 +19,24 @@ Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
Require Export Coq.Init.Tauto.
-(* Initially available plugins
- (+ nat_syntax_plugin loaded in Datatypes) *)
+(* Some initially available plugins. See also:
+ - ltac_plugin (in Notations)
+ - tauto_plugin (in Tauto).
+*)
Declare ML Module "cc_plugin".
Declare ML Module "ground_plugin".
+Declare ML Module "numeral_notation_plugin".
+
+(* Parsing / printing of decimal numbers *)
+Arguments Nat.of_uint d%dec_uint_scope.
+Arguments Nat.of_int d%dec_int_scope.
+Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+ : dec_uint_scope.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+ : dec_int_scope.
+
+(* Parsing / printing of [nat] numbers *)
+Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+
(* Default substrings not considered by queries like SearchAbout *)
Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 1ee098cb07..4f2fdcf94c 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -333,7 +333,7 @@ Proof.
auto with set.
Qed.
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
Lemma union_subset_1: subset s (union s s')=true.
Proof.
@@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2.
rewrite not_mem_iff; auto.
Qed.
-(* caracterisation of [union] via [subset] *)
+(* characterisation of [union] via [subset] *)
Lemma inter_subset_1: subset (inter s s') s=true.
Proof.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 9d2a73ed0f..95868861fa 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -13,7 +13,7 @@
This module factorizes common parts in implementations
of finite sets as AVL trees and as Red-Black trees. The nodes
of the trees defined here include an generic information
- parameter, that will be the heigth in AVL trees and the color
+ parameter, that will be the height in AVL trees and the color
in Red-Black trees. Without more details here about these
information parameters, trees here are not known to be
well-balanced, but simply binary-search-trees.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5d3ec5abc7..bd27f94abd 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N.
(** Exportation of notations *)
+Numeral Notation N N.of_uint N.to_uint : N_scope.
+
Infix "+" := N.add : N_scope.
Infix "-" := N.sub : N_scope.
Infix "*" := N.mul : N_scope.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 5de75537cb..be12fffaaf 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -13,6 +13,10 @@ Require Import BinPos.
Local Open Scope N_scope.
+Local Notation "0" := N0.
+Local Notation "1" := (Npos 1).
+Local Notation "2" := (Npos 2).
+
(**********************************************************************)
(** * Binary natural numbers, definitions of operations *)
(**********************************************************************)
@@ -398,4 +402,9 @@ Definition to_uint n :=
Definition to_int n := Decimal.Pos (to_uint n).
+Numeral Notation N of_uint to_uint : N_scope.
+
End N.
+
+(** Re-export the notation for those who just [Import NatIntDef] *)
+Numeral Notation N N.of_uint N.to_uint : N_scope.
diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
new file mode 100644
index 0000000000..c7e3999691
--- /dev/null
+++ b/theories/Numbers/AltBinNotations.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \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) *)
+(************************************************************************)
+
+(** * Alternative Binary Numeral Notations *)
+
+(** Faster but less safe parsers and printers of [positive], [N], [Z]. *)
+
+(** By default, literals in types [positive], [N], [Z] are parsed and
+ printed via the [Numeral Notation] command, by conversion from/to
+ 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
+ Notation] commmands that use [Z] as bridge type. To enable these
+ commands, just be sure to [Require] this file after other files
+ defining numeral notations.
+
+ Note: up to Coq 8.8, literals in types [positive], [N], [Z] were
+ parsed and printed using a native ML library of arbitrary
+ precision integers named bigint.ml. From 8.9, the default is to
+ parse and print using a Coq library converting sequences of
+ digits, hence reducing the amount of ML code to trust. But this
+ method is slower. This file then gives access to the legacy
+ method, trading efficiency against a larger ML trust base relying
+ on bigint.ml. *)
+
+Require Import BinNums.
+
+(** [positive] *)
+
+Definition pos_of_z z :=
+ match z with
+ | Zpos p => Some p
+ | _ => None
+ end.
+
+Definition pos_to_z p := Zpos p.
+
+Numeral Notation positive pos_of_z pos_to_z : positive_scope.
+
+(** [N] *)
+
+Definition n_of_z z :=
+ match z with
+ | Z0 => Some N0
+ | Zpos p => Some (Npos p)
+ | Zneg _ => None
+ end.
+
+Definition n_to_z n :=
+ match n with
+ | N0 => Z0
+ | Npos p => Zpos p
+ end.
+
+Numeral Notation N n_of_z n_to_z : N_scope.
+
+(** [Z] *)
+
+Definition z_of_z (z:Z) := z.
+
+Numeral Notation Z z_of_z z_of_z : Z_scope.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index d5eb4f2681..3ba9d1f5ed 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -12,15 +12,11 @@
Set Implicit Arguments.
-Declare ML Module "positive_syntax_plugin".
-Declare ML Module "n_syntax_plugin".
-Declare ML Module "z_syntax_plugin".
-
(** [positive] is a datatype representing the strictly positive integers
in a binary way. Starting from 1 (represented by [xH]), one can
add a new least significant digit via [xO] (digit 0) or [xI] (digit 1).
- Numbers in [positive] can also be denoted using a decimal notation;
- e.g. [6%positive] abbreviates [xO (xI xH)] *)
+ Numbers in [positive] will also be denoted using a decimal notation;
+ e.g. [6%positive] will abbreviate [xO (xI xH)] *)
Inductive positive : Set :=
| xI : positive -> positive
@@ -34,8 +30,8 @@ Arguments xI _%positive.
(** [N] is a datatype representing natural numbers in a binary way,
by extending the [positive] datatype with a zero.
- Numbers in [N] can also be denoted using a decimal notation;
- e.g. [6%N] abbreviates [Npos (xO (xI xH))] *)
+ Numbers in [N] will also be denoted using a decimal notation;
+ e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *)
Inductive N : Set :=
| N0 : N
@@ -49,8 +45,8 @@ Arguments Npos _%positive.
An integer is either zero or a strictly positive number
(coded as a [positive]) or a strictly negative number
(whose opposite is stored as a [positive] value).
- Numbers in [Z] can also be denoted using a decimal notation;
- e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *)
+ Numbers in [Z] will also be denoted using a decimal notation;
+ e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *)
Inductive Z : Set :=
| Z0 : Z
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index bd4f0279d4..ec480bb1eb 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -23,8 +23,6 @@ Require Import Zpow_facts.
Require Import CyclicAxioms.
Require Import ROmega.
-Declare ML Module "int31_syntax_plugin".
-
Local Open Scope nat_scope.
Local Open Scope int31_scope.
@@ -128,7 +126,7 @@ Section Basics.
Lemma nshiftl_S_tail :
forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof.
+ Proof.
intros n; elim n; simpl; intros; now f_equal.
Qed.
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 9f8da831d8..39af62c32f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,6 +15,8 @@ Require Import Wf_nat.
Require Export ZArith.
Require Export DoubleType.
+Declare ML Module "int31_syntax_plugin".
+
(** * 31-bit integers *)
(** This file contains basic definitions of a 31-bit integer
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 2da4452819..4aabda77ee 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -80,7 +80,7 @@ Proof.
now apply testbit_even_succ.
Qed.
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
(** This concise equation could have been taken as specification
for testbit in the interface, but it would have been hard to
@@ -102,10 +102,10 @@ Proof.
left. destruct b; split; simpl; order'.
Qed.
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
power was initially taken as specification for testbit.
We describe [a] as having a low part and a high part, with
- the corresponding bit in the middle. This caracterisation
+ the corresponding bit in the middle. This characterisation
is moderatly complex to implement, but also moderately
usable... *)
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index e1391f5990..90663de3f2 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -78,7 +78,7 @@ Proof.
apply testbit_even_succ, le_0_l.
Qed.
-(** Alternative caracterisations of [testbit] *)
+(** Alternative characterisations of [testbit] *)
(** This concise equation could have been taken as specification
for testbit in the interface, but it would have been hard to
@@ -99,10 +99,10 @@ Proof.
destruct b; order'.
Qed.
-(** This caracterisation that uses only basic operations and
+(** This characterisation that uses only basic operations and
power was initially taken as specification for testbit.
We describe [a] as having a low part and a high part, with
- the corresponding bit in the middle. This caracterisation
+ the corresponding bit in the middle. This characterisation
is moderatly complex to implement, but also moderately
usable... *)
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 000d895e10..dcaae1606d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive.
(** Exportation of notations *)
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
+
Infix "+" := Pos.add : positive_scope.
Infix "-" := Pos.sub : positive_scope.
Infix "*" := Pos.mul : positive_scope.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 070314746a..7f30733559 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -26,6 +26,8 @@ Require Export BinNums.
for the number 6 (which is 110 in binary notation).
*)
+Local Notation "1" := xH.
+
Notation "p ~ 1" := (xI p)
(at level 7, left associativity, format "p '~' '1'") : positive_scope.
Notation "p ~ 0" := (xO p)
@@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p :=
let r' := g (f r) in
if s' <=? r' then (s~1, sub_mask r' s')
else (s~0, IsPos r')
- | (s,_) => (s~0, sub_mask (g (f 1)) 4)
+ | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0)
end.
Fixpoint sqrtrem p : positive * mask :=
match p with
| 1 => (1,IsNul)
- | 2 => (1,IsPos 1)
- | 3 => (1,IsPos 2)
+ | 1~0 => (1,IsPos 1)
+ | 1~1 => (1,IsPos 1~0)
| p~0~0 => sqrtrem_step xO xO (sqrtrem p)
| p~0~1 => sqrtrem_step xO xI (sqrtrem p)
| p~1~0 => sqrtrem_step xI xO (sqrtrem p)
@@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p).
Definition to_int n := Decimal.Pos (to_uint n).
+Numeral Notation positive of_int to_uint : positive_scope.
+
End Pos.
+
+(** Re-export the notation for those who just [Import BinPosDef] *)
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 6a3dd97656..9b8dd1db0b 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool :=
| right _ => false
end.
-(** Sequential caracterisation of continuity *)
+(** Sequential characterisation of continuity *)
Lemma continuity_seq :
forall (f:R -> R) (Un:nat -> R) (l:R),
continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 05edc6ccde..4d04667c01 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -83,7 +83,7 @@ End GenericMinMax.
Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
Module Import Private_Tac := !MakeOrderTac O O.
-(** An alternative caracterisation of [max], equivalent to
+(** An alternative characterisation of [max], equivalent to
[max_l /\ max_r] *)
Lemma max_spec n m :
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index cf7397b57e..a11d491a8b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z.
(** Re-export Notations *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+
Infix "+" := Z.add : Z_scope.
Notation "- x" := (Z.opp x) : Z_scope.
Infix "-" := Z.sub : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index db4de0b90c..8cb62622db 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -14,6 +14,10 @@ Require Import BinPos BinNat.
Local Open Scope Z_scope.
+Local Notation "0" := Z0.
+Local Notation "1" := (Zpos 1).
+Local Notation "2" := (Zpos 2).
+
(***********************************************************)
(** * Binary Integers, Definitions of Operations *)
(***********************************************************)
@@ -53,7 +57,7 @@ Definition succ_double x :=
Definition pred_double x :=
match x with
- | 0 => -1
+ | 0 => neg 1
| neg p => neg p~1
| pos p => pos (Pos.pred_double p)
end.
@@ -104,7 +108,7 @@ Definition succ x := x + 1.
(** ** Predecessor *)
-Definition pred x := x + -1.
+Definition pred x := x + neg 1.
(** ** Subtraction *)
@@ -171,7 +175,7 @@ Definition sgn z :=
match z with
| 0 => 0
| pos p => 1
- | neg p => -1
+ | neg p => neg 1
end.
(** Boolean equality and comparisons *)
@@ -635,4 +639,9 @@ Definition lxor a b :=
| neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
end.
+Numeral Notation Z of_int to_int : Z_scope.
+
End Z.
+
+(** Re-export the notation for those who just [Import BinIntDef] *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:19:03 +0000