commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 9a7e24e0875776b22cacc5b7ab7229b5fb9d5ee2..2c98ad147c621a560b3ad8c47ad00fface2a0ab4 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,5 +1,6 @@
-(* In this Chapter we shall develop a naif theory of sets represented as characteristic
-predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop. *)
+(* In this Chapter we shall develop a naif theory of sets represented as 
+characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type 
+A→Prop. *)
 
 include "basics/types.ma".
 include "basics/bool.ma".
@@ -244,18 +245,18 @@ example exhint: ∀b:\ 5a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"\ 6DeqB
 #b #H @(\P H) 
 qed.
 
-(* The point is that == expects in input a pair of objects object whose type 
-must be the carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the 
-type inference system has no knowledge of it (it is an information that has been
-supplied by the user, and stored somewhere in the library). More explicitly, the
-type inference inference system, would face an unification problem consisting to
-unify bool against the carrier of something (a metavaribale) and it has no way to
-synthetize the answer. To solve this kind of situations, matita provides a 
-mechanism to hint the system the expected solution. A unification hint is a kind of
-rule, whose rhd is the unification problem, containing some metavariables X1, ...,
-Xn, and whose left hand side is the solution suggested to the system, in the form
-of equations Xi=Mi. The hint is accepted by the system if and only the solution is
-correct, that is, if it is a unifier for the given problem.
+(* The point is that == expects in input a pair of objects whose type must be the 
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference 
+system has no knowledge of it (it is an information that has been supplied by the 
+user, and stored somewhere in the library). More explicitly, the type inference 
+inference system, would face an unification problem consisting to unify bool 
+against the carrier of something (a metavaribale) and it has no way to synthetize 
+the answer. To solve this kind of situations, matita provides a mechanism to hint 
+the system the expected solution. A unification hint is a kind of rule, whose rhd 
+is the unification problem, containing some metavariables X1, ..., Xn, and whose 
+left hand side is the solution suggested to the system, in the form of equations 
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.
 To make an example, in the previous case, the unification problem is bool = carr X,
 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since 
 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
@@ -270,8 +271,8 @@ unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a
 (* ---------------------------------------- *) ⊢ 
     \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X b1 b2.
     
-(* After having provided the previous hints, we may rewrite example exhint delcaring
-b of type bool. *)
+(* After having provided the previous hints, we may rewrite example exhint 
+declaring b of type bool. *)
  
 example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. (b \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6. 
 #b #H @(\P H)