commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index eeedb14bb31997a3fb64dc6ff0112bda04c71f89..85815e006cb566b40ae971bbbde955cc223b9d0e 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -30,7 +30,7 @@ match n with
 
 (* It is worth to observe that the previous algorithm works by recursion over the first 
 argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)
 
 (* It is worth to observe that the previous algorithm works by recursion over the first 
 argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)

-is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it 
+is stuck. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it 

 is called induction. The induction principle states that, given a property P(n) over natural 
 numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
 P(n) for any n. 
 is called induction. The induction principle states that, given a property P(n) over natural 
 numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
 P(n) for any n.