From f3352e5e2187c2b7074625e15de4ea0a293d1d4c Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 28 Oct 2011 14:37:01 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 -- 2.39.2