commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index ca7e89355b9e9bf5fcf98d772056a4c5b6a50dd3..228bffd513f42f264c6e83f8742e08c4c3c0e0d2 100644 (file)
--- 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