X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=eeedb14bb31997a3fb64dc6ff0112bda04c71f89;hb=2eabadeaefa733670225ae6c931ec5ed45b44b10;hp=7a60a7b523412e27c92cf035739a1bb5a7ed4d5f;hpb=948676ae86382ebdfd13b7d485da02137cce558d;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 7a60a7b52..eeedb14bb 100644
--- 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.