diff options
| -rw-r--r-- | theories/NArith/BinNat.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 222f6de2fa..4d3d30f212 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -15,6 +15,17 @@ Require BinPos. Inductive entier: Set := Nul : entier | Pos : positive -> entier. +(** Declare binding key for scope positive_scope *) + +Delimits Scope N_scope with N. + +(** Automatically open scope N_scope for the constructors of N *) + +Bind Scope N_scope with entier. +Arguments Scope Pos [ N_scope ]. + +Open Local Scope N_scope. + (** Operation x -> 2*x+1 *) Definition Un_suivi_de := [x] @@ -39,6 +50,8 @@ Definition Nplus := [n,m] | (Pos p) (Pos q) => (Pos (add p q)) end. +V8Infix "+" Nplus : N_scope. + (** Multiplication *) Definition Nmult := [n,m] @@ -48,6 +61,8 @@ Definition Nmult := [n,m] | (Pos p) (Pos q) => (Pos (times p q)) end. +V8Infix "*" Nmult : N_scope. + (** Order *) Definition Ncompare := [n,m] @@ -58,6 +73,8 @@ Definition Ncompare := [n,m] | (Pos n') (Pos m') => (compare n' m' EGAL) end. +V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope. + (** Peano induction on binary natural numbers *) Theorem Nind : (P:(entier ->Prop)) |