commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 7a60a7b523412e27c92cf035739a1bb5a7ed4d5f..eeedb14bb31997a3fb64dc6ff0112bda04c71f89 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -217,9 +217,9 @@ specification into a single entity. The idea is to refine the output type of the
 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a specific 
 pair satisfying the specification of the function. In other words, we need the
 possibility to define, for a type A and a property P over A, the subset type 
-{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset type are
+{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types are
 just a particular case of the so called dependent types, that is types that can 
-depend over arguments (such as arrays of a specified lenght, taken as a parameter).
+depend over arguments (such as arrays of a specified length, taken as a parameter).
 These kind of types are quite unusual in traditional programming languages, and their
 study is one of the new frontiers of the current research on type systems.