diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 02:28:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-10 02:28:43 +0000 |
| commit | 952d9ebd44fe6bd052c81c583e3a74752b53f932 (patch) | |
| tree | ecc5842e59ae2f75c7a2b35fdc54f1106664803e /theories/NArith/BinNat.v | |
| parent | 5e475019abd6ac3a8bb923b6133625da446696c2 (diff) | |
Proposal of a nice notation for constructors xI and xO of type positive
More details in the header of BinPos.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/BinNat.v')
| -rw-r--r-- | theories/NArith/BinNat.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index d0ed874dd..9949d612d 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -148,7 +148,7 @@ Defined. Definition Ndouble_plus_one x := match x with | N0 => Npos 1 -| Npos p => Npos (xI p) +| Npos p => Npos p~1 end. (** Operation x -> 2 * x *) @@ -156,7 +156,7 @@ end. Definition Ndouble n := match n with | N0 => N0 -| Npos p => Npos (xO p) +| Npos p => Npos p~0 end. (** convenient induction principles *) @@ -193,8 +193,8 @@ Definition Ndiv2 (n:N) := match n with | N0 => N0 | Npos 1 => N0 - | Npos (xO p) => Npos p - | Npos (xI p) => Npos p + | Npos p~0 => Npos p + | Npos p~1 => Npos p end. Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. |