From: matitaweb Date: Wed, 7 Mar 2012 11:50:55 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1877 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f09ad987d622554030aafe383a4396c95899ec91;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 20762a99a..83a1c28d8 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -225,7 +225,9 @@ DeqSet is decidable in the traditional sense, namely either a=b or a≠b *) [%1 @(\P H) | %2 @(\Pf H)] qed. -(* A simple example of a set with a decidable equality is bool. We first define +(* +h2 class="section"Unification Hints/h2 +A simple example of a set with a decidable equality is bool. We first define the boolean equality beqb, that is just the xand function, then prove that beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by instantiating the DeqSet record with the previous information *) @@ -241,9 +243,7 @@ qed. definition DeqBool ≝ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a. -(* -h2 class="section"Unification Hints/h2 -At this point, we would expect to be able to prove things like the +(* At this point, we would expect to be able to prove things like the following: for any boolean b, if b==false is true then b=false. Unfortunately, this would not work, unless we declare b of type DeqBool (change the type in the following statement and see what