From: matitaweb Date: Tue, 11 Oct 2011 16:24:14 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2211 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f498c284f96d3b6fe47c4ccd1c834bcadd80c82a;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 2de8f8558..d309eeed2 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -18,7 +18,7 @@ O, S O, S (S O), S (S (S O)) and so on. The language of Matita allows the definition of well founded recursive functions over inductive types; in order to guarantee termination of recursion you are only allowed to make recursive -calls on structurally smaller arguments than the ones your received in input. +calls on structurally smaller arguments than the 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 *)