X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter7.ma;h=17316f03169fc9a3707999b29b69298d9612ab8a;hb=a2ba04cd90e76937720b16e37cb12a39b46181e3;hp=a4e3a861472a54c5c207646ecb2c0ffcd5067fa5;hpb=7956b9a84e0556d2d24fffedbbbabcd9e248d702;p=helm.git

diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index a4e3a8614..17316f031 100644
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -31,11 +31,11 @@ interpretation "empty" 'empty = (z ?).
 (* The language sem{e} associated with the regular expression e is inductively 
 defined by the following function: *)
 
-let rec in_l (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (r : a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop ≝ 
+let rec in_l (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span) (r : a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/aspan class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"/span S → Prop ≝ 
 match r with
 [ z ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a
 | e ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}
-| s x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) }
+| s x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/aspan class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"/span (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) }
 | c r1 r2 ⇒ (in_l ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a (in_l ? r2)
 | o r1 r2 ⇒ (in_l ? r1) a title="union" href="cic:/fakeuri.def(1)"∪/a (in_l ? r2)
 | k r1 ⇒ (in_l ? r1) a title="star lang" href="cic:/fakeuri.def(1)"^/a*].
@@ -116,7 +116,7 @@ let rec forget (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"Deq
   | ps x ⇒ a title="atom" href="cic:/fakeuri.def(1)"`/ax
   | pp x ⇒ a title="atom" href="cic:/fakeuri.def(1)"`/ax
   | pc E1 E2 ⇒ (forget ? E1) a title="re cat" href="cic:/fakeuri.def(1)"·/a (forget ? E2)
-  | po E1 E2 ⇒ (forget ? E1) a title="re or" href="cic:/fakeuri.def(1)"+/a (forget ? E2)
+  | po E1 E2 ⇒ (forget ? E1) a title="re or" href="cic:/fakeuri.def(1)"+/aspan class="error" title="Parse error: [term] expected after [sym+] (in [term])"/span (forget ? E2)
   | pk E ⇒ (forget ? E)a title="re star" href="cic:/fakeuri.def(1)"^/a* ].
  
 (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
@@ -147,7 +147,7 @@ let rec beqitem S (i1,i2: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1
   | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1a title="eqb" href="cic:/fakeuri.def(1)"=/a=y2 | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a]
   | po i11 i12 ⇒ match i2 with 
     [ po i21 i22 ⇒ beqitem S i11 i21 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a beqitem S i12 i22
-    | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a]
+    | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aspan class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"/span]
   | pc i11 i12 ⇒ match i2 with 
     [ pc i21 i22 ⇒ beqitem S i11 i21 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a beqitem S i12 i22
     | _ ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a]
@@ -213,7 +213,7 @@ match r with
 | pe ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a
 | ps _ ⇒ a title="empty set" href="cic:/fakeuri.def(1)"∅/a
 | pp x ⇒ a title="singleton" href="cic:/fakeuri.def(1)"{/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) }
-| pc r1 r2 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r2} a title="union" href="cic:/fakeuri.def(1)"∪/a (in_pl ? r2)
+| pc r1 r2 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r2} a title="union" href="cic:/fakeuri.def(1)"∪/aspan class="error" title="Parse error: [term] expected after [sym∪] (in [term])"/span (in_pl ? r2)
 | po r1 r2 ⇒ (in_pl ? r1) a title="union" href="cic:/fakeuri.def(1)"∪/a (in_pl ? r2)
 | pk r1 ⇒ (in_pl ? r1) a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"forget/a ? r1}a title="star lang" href="cic:/fakeuri.def(1)"^/a*  ].
 
@@ -295,7 +295,7 @@ lemma minus_eps_item: ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind
   ]
 qed.
 
-lemma minus_eps_pre: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e}a title="substraction" href="cic:/fakeuri.def(1)"-/aa title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]}.
+lemma minus_eps_pre: ∀S.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_pl" href="cic:/fakeuri.def(1)"\sem/aspan class="error" title="Parse error: [sym{] expected after [sym\sem ] (in [term])"/span{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e}a title="substraction" href="cic:/fakeuri.def(1)"-/aa title="singleton" href="cic:/fakeuri.def(1)"{/aa title="nil" href="cic:/fakeuri.def(1)"[/a ]}.
 #S * #i * 
   [>a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"sem_pre_true/a normalize in ⊢ (??%?); #w % 
     [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ | * * // #H1 #H2 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a …H1 H2)]