From 5d546aa7717884c1d5ceebee24ad044894ebbfcb Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 14 Oct 2011 14:31:37 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index eeedb14bb..85815e006 100644 --- 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) -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. -- 2.39.2