From: matitaweb Date: Wed, 12 Oct 2011 11:41:37 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2204 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34b7023a76f83ffbd489e4a59bb068ef0f5e7c36;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index ec3724cd8..21a0151cd 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -210,6 +210,11 @@ depend over arguments (such as arrays of a specified lenght, taken as a paramete 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. +There is nothing special in a subset type {a:A|P(a)}: it is just a record composed by +an element of a of type A and a proof of P(a). The crucial point is to have a language +reach enough to comprise proofs among its expressions. *) +axiom div2P n : nat → {N×N | True}. +