From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Feb 2012 13:55:24 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1930
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bef004f9c2ab68f9f0f9c95536918681a61849fc

commit by user andrea
---

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 2c98ad147..c159fa13d 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -278,7 +278,10 @@ example exhint1: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a
 #b #H @(\P H)
 qed.
 
-(* pairs *)
+(* The cartesian product of two DeqSets is still a DeqSet. To prove
+this, we must as usual define the boolen equality function, and prove
+it correctly reflects propositional equality. *)
+
 definition eq_pairs ≝
   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 
@@ -292,7 +295,12 @@ qed.
 
 definition DeqProd ≝ λA,B:DeqSet.
   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-  
+
+(* Having an unification problem of the kind T1×T2 = carr X, what kind 
+of hint can we give to the system? We expect T1 to be the carrier of a
+DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
+This is expressed by the following hint: *)
+
 unification hint  0 ≔ C1,C2; 
     T1 ≟ carr C1,
     T2 ≟ carr C2,