From f498c284f96d3b6fe47c4ccd1c834bcadd80c82a Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 11 Oct 2011 16:24:14 +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 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 *) -- 2.39.2