From f09ad987d622554030aafe383a4396c95899ec91 Mon Sep 17 00:00:00 2001 From: matitaweb <claudio.sacerdoticoen@unibo.it> Date: Wed, 7 Mar 2012 11:50:55 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.5