diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 08:58:09 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 08:58:09 +0000 |
commit | d6e4d2e96e6ddd5168ce44ae556b63302044e697 (patch) | |
tree | b4a0f64ff00d625bf81e37939b7d935dd5e53b88 | |
parent | 8fcabcc22e256f5b484532882a23714a9607c684 (diff) |
Essai d'utilisation de 'where' pour les notations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | theories/Init/Peano.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index b4ce93819..cd531f150 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -89,13 +89,14 @@ Hint Resolve n_Sn: core v62. Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m - | S p => S (plus p m) - end. + | S p => S (p + m) + end + +where "n + m" := (plus n m) : nat_scope. + Hint Resolve (f_equal2 plus): v62. Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. -Infix "+" := plus : nat_scope. - Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl in |- *; auto. @@ -123,11 +124,12 @@ Qed. Fixpoint mult (n m:nat) {struct n} : nat := match n with | O => 0 - | S p => m + mult p m - end. -Hint Resolve (f_equal2 mult): core v62. + | S p => m + p * m + end -Infix "*" := mult : nat_scope. +where "n * m" := (mult n m) : nat_scope. + +Hint Resolve (f_equal2 mult): core v62. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. @@ -149,10 +151,10 @@ Fixpoint minus (n m:nat) {struct n} : nat := match n, m with | O, _ => 0 | S k, O => S k - | S k, S l => minus k l - end. + | S k, S l => k - l + end -Infix "-" := minus : nat_scope. +where "n - m" := (minus n m) : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] can be found in files Le and Lt *) |