commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index ec3724cd8049a51b34811e5720b9708ae37d5e36..21a0151cd2f4b17aac12bc916f9a95a28291a241 100644 (file)
--- 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. 
 
 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}.
+