Changeset 1516 for src/common/Identifiers.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (8 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/common/Identifiers.ma (modified) (4 diffs)

src/common/Identifiers.ma

@@ -56 +56 @@
 
 lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
-#tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
+#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
 qed.
 
@@ -64 +64 @@
 
 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
-#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
+#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
 #E [ % | %2 ]
 lapply E @eqb_elim
@@ -184 +184 @@
   ] (refl ? u').
 cases l in p E; cases m; -l' -m' #m' #l'
-whd in ⊢ (% → ?)
- whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
+whd in ⊢ (% → ?);
+ whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
 #NL #U cases NL #H @H @(update_fail … U)
 qed.
@@ -194 +194 @@
   present tag A (update_present tag A m id' H' a) id.
 #tag #A * #m * #id #a * #id' #H #H'
-whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
+whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
 cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
-[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
+[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
   % #E' destruct
-| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
+| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
   <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
 ] qed.