commit by user andrea

[helm.git] / weblib / tutorial / chapter5.ma

diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma
index a3b88978ba5d9c08b33c23bea8c06d1a31432692..014cb611f94cdc7be6eecc41beaa6479f23a2421 100644 (file)
--- a/weblib/tutorial/chapter5.ma
+++ b/weblib/tutorial/chapter5.ma
@@ -4,7 +4,7 @@ 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 
 a DeqSet, and prove some of their properties.*)
 
-include "basics/list.ma".
+include "basics/list.ma". 
 include "tutorial/chapter4.ma".
 
 (* The first function we define is an effective version of the membership relation,
@@ -14,8 +14,8 @@ l.*)
 let rec memb (S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6 S) on l  ≝
   match l with
   [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
-  | cons a tl ⇒ (x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6= a) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 memb S x tl
-  ].
+  | cons a tl ⇒ (x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= a) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 memb S x tl
+  ]\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="No choices for ID nil"\ 6\ 5/span\ 6.
 
 notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
 interpretation "boolean membership" 'memb a l = (memb ? a l).
@@ -51,7 +51,7 @@ qed.
 
 lemma memb_append: ∀S,a,l1,l2. 
 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5span class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"\ 6\ 5/span\ 6l2) \ 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 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 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 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 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.
-#S #a #l1 elim l1 normalize [#l2 #H %2 //] 
+#S #a #l1\ 5span class="error" title="Parse error: illegal begin of statement"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: illegal begin of statement"\ 6\ 5/span\ 6 elim l1 normalize [#l2 #H %2 //] 
 #b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 
 qed.