From: matitaweb Date: Thu, 8 Mar 2012 07:21:22 +0000 (+0000) Subject: Sectionin X-Git-Tag: make_still_working~1875 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63ffd77b87eed31ea50ba0260c6e885abe8c552b;p=helm.git Sectionin --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 83a1c28d8..32a3f23ea 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -44,14 +44,16 @@ sets *) definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a). interpretation "subset" 'subseteq a b = (subset ? a b). -(* Two sets are equals if and only if they have the same elements, that is, +(* h2 class="section"Set Quality/h2 +Two sets are equals if and only if they have the same elements, that is, if the two characteristic functions are extensionally equivalent: *) definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a a title="iff" href="cic:/fakeuri.def(1)"↔/aspan class="error" title="Parse error: [term] expected after [sym↔] (in [term])"/span Q a. notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}. interpretation "extensional equality" 'eqP a b = (eqP ? a b). -(* This notion of equality is different from the intensional equality of +(* +This notion of equality is different from the intensional equality of functions; the fact it defines an equivalence relation must be explicitly proved: *) diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index 014cb611f..f0c497707 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -1,4 +1,6 @@ -(* The fact of being able to decide, via a computable boolean function, the +(* +h1 class="section"Effective searching/h1 +The fact of being able to decide, via a computable boolean function, the equality between elements of a given set is an essential prerequisite for effectively searching an element of that set inside a data structure. In this section we shall define several boolean functions acting on lists of elements in