X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter2.ma;h=1f0244505e3d54333a795f27f16da66ed5686507;hb=278be9d611634dce13657bbe14b5c1bb4f7dd2be;hp=14ae1b679e4e10b77eee87baa181937562148670;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma
index 14ae1b679..1f0244505 100644
--- a/matita/matita/lib/tutorial/chapter2.ma
+++ b/matita/matita/lib/tutorial/chapter2.ma
@@ -29,11 +29,9 @@ follows: *)
 let rec add n (m:nat) ≝ 
 match n with
 [ O ⇒ m
-| S a ⇒ add (S a) m
+| S a ⇒ S (add a m)
 ].
 
-check 
-
 (* Observe that the definition of a recursive function requires the keyword 
 "let rec" instead of "definition". The specification of formal parameters is 
 different too. In this case, they come before the body, and do not require a λ. 
@@ -375,3 +373,20 @@ normalize // qed.
 example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O)))))) 
        = 〈twice (twice (twice (S O))), ff〉.
 // qed. 
+
+(********************)
+
+inductive Pari : nat → Prop ≝
+   | pariO : Pari O
+   | pari2 : ∀x. Pari x → Pari (S (S x)).
+   
+definition natPari ≝ Sub nat Pari.
+
+definition addPari: natPari → natPari → natPari.
+* #a #Ha * #b #Hb @(mk_Sub … (add a b))  
+elim Ha
+  [normalize @Hb
+  |#x #Hx #Hind normalize @pari2 @Hind
+  ]
+qed.    
+