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. 
 
+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}.
+