chapters 2 e 3

[helm.git] / matita / matita / lib / tutorial / chapter2.ma

diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma
index 7dda6e6f2c9bc2f06d55d530cf95de96465a6df8..14ae1b679e4e10b77eee87baa181937562148670 100644 (file)
--- a/matita/matita/lib/tutorial/chapter2.ma
+++ b/matita/matita/lib/tutorial/chapter2.ma
@@ -26,12 +26,14 @@ ones you received in input. Most mathematical functions can be naturally defined
 in this way. For instance, the sum of two natural numbers can be defined as 
 follows: *)
 
-let rec add n m ≝ 
+let rec add n (m:nat) ≝ 
 match n with
 [ O ⇒ m
-| S a ⇒ S (add a m)
+| S a ⇒ add (S 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 λ.