summaryrefslogtreecommitdiff
path: root/theories/NArith/BinNat.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/NArith/BinNat.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/NArith/BinNat.v')
-rw-r--r--theories/NArith/BinNat.v17
1 files changed, 9 insertions, 8 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index e6a14938..b4582d51 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -6,9 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: BinNat.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
+(*i $Id: BinNat.v 8685 2006-04-06 13:22:02Z letouzey $ i*)
Require Import BinPos.
+Unset Boxed Definitions.
(**********************************************************************)
(** Binary natural numbers *)
@@ -21,10 +22,10 @@ Inductive N : Set :=
Delimit Scope N_scope with N.
-(** Automatically open scope N_scope for the constructors of N *)
+(** Automatically open scope positive_scope for the constructors of N *)
Bind Scope N_scope with N.
-Arguments Scope Npos [N_scope].
+Arguments Scope Npos [positive_scope].
Open Local Scope N_scope.
@@ -32,7 +33,7 @@ Open Local Scope N_scope.
Definition Ndouble_plus_one x :=
match x with
- | N0 => Npos 1%positive
+ | N0 => Npos 1
| Npos p => Npos (xI p)
end.
@@ -47,7 +48,7 @@ Definition Ndouble n := match n with
Definition Nsucc n :=
match n with
- | N0 => Npos 1%positive
+ | N0 => Npos 1
| Npos p => Npos (Psucc p)
end.
@@ -57,7 +58,7 @@ Definition Nplus n m :=
match n, m with
| N0, _ => m
| _, N0 => n
- | Npos p, Npos q => Npos (p + q)%positive
+ | Npos p, Npos q => Npos (p + q)
end.
Infix "+" := Nplus : N_scope.
@@ -68,7 +69,7 @@ Definition Nmult n m :=
match n, m with
| N0, _ => N0
| _, N0 => N0
- | Npos p, Npos q => Npos (p * q)%positive
+ | Npos p, Npos q => Npos (p * q)
end.
Infix "*" := Nmult : N_scope.
@@ -154,7 +155,7 @@ Qed.
(** Properties of multiplication *)
-Theorem Nmult_1_l : forall n:N, Npos 1%positive * n = n.
+Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
Proof.
destruct n; reflexivity.
Qed.