From 2eabadeaefa733670225ae6c931ec5ed45b44b10 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Fri, 14 Oct 2011 08:05:26 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2