]> matita.cs.unibo.it Git - helm.git/commitdiff
commit by user andrea
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Fri, 14 Oct 2011 14:31:37 +0000 (14:31 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Fri, 14 Oct 2011 14:31:37 +0000 (14:31 +0000)
weblib/tutorial/chapter2.ma

index eeedb14bb31997a3fb64dc6ff0112bda04c71f89..85815e006cb566b40ae971bbbde955cc223b9d0e 100644 (file)
@@ -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)
-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.