Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1515 r1516  
    5656
    5757lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
    58 #tag * #id whd in ⊢ (??%?) >eqb_n_n @refl
     58#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
    5959qed.
    6060
     
    6464
    6565definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
    66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
     66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
    6767#E [ % | %2 ]
    6868lapply E @eqb_elim
     
    184184  ] (refl ? u').
    185185cases l in p E; cases m; -l' -m' #m' #l'
    186 whd in ⊢ (% → ?)
    187  whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
     186whd in ⊢ (% → ?);
     187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
    188188#NL #U cases NL #H @H @(update_fail … U)
    189189qed.
     
    194194  present tag A (update_present tag A m id' H' a) id.
    195195#tag #A * #m * #id #a * #id' #H #H'
    196 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     196whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
    197197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
    198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
     198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
    199199  % #E' destruct
    200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
     200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
    201201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    202202] qed.
Note: See TracChangeset for help on using the changeset viewer.