From: matitaweb Date: Fri, 28 Oct 2011 14:37:01 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2147 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3352e5e2187c2b7074625e15de4ea0a293d1d4c;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index ca7e89355..228bffd51 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -10,11 +10,11 @@ inductive list (A:Type[0]) : Type[0] ≝ | cons: A -> list A -> list A. (* The type notation list A is the type of all lists with elements of type A: it is -defined by tow constructors: a polymorphic empty list (nil A) and a cons operation, +defined by two constructors: a polymorphic empty list (nil A) and a cons operation, adding a new head element of type A to a previous list. For instance, (list nat) and and (list bool) are lists of natural numbers and booleans, respectively. But we can -also form more complex data typea, like (list (list (nat → nat))), that is a list whose -elements are lists of functions from natural number to natural numbers. +also form more complex data types, like (list (list (nat → nat))), that is a list whose +elements are lists of functions from natural numbers to natural numbers. Typical elements in (list bool) are for instance, nil nat - the empty list of type nat