From: matitaweb Date: Fri, 14 Oct 2011 08:05:26 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2189 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2eabadeaefa733670225ae6c931ec5ed45b44b10;p=helm.git commit by user andrea --- 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.