Changeset 1516 for src/common/AST.ma


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/AST.ma

    r1465 r1516  
    145145lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
    146146  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
    147 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     147* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
    148148qed.
    149149
     
    175175  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
    176176#A * * #P #p #f #d #Q #Hne #Heq
    177 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
    178 | *: whd in ⊢ (?%) @Hne % #E destruct
     177[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
     178| *: whd in ⊢ (?%); @Hne % #E destruct
    179179] qed.
    180180
     
    351351 #A #B #C #f #l elim l
    352352  [ #l' #E normalize in E; destruct %
    353   | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
     353  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
    354354    [2: #err #E destruct
    355355    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
    356       cases (map_partial … f tl) in IH ⊢ %
    357       #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize
     356      cases (map_partial … f tl) in IH ⊢ %;
     357      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
    358358      >(IH x) // ]]
    359359qed.
     
    487487 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
    488488 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
    489    #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ % >e0 //
     489   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
    490490   >e0 in e1; normalize #H @H ]
    491491qed.
     
    498498  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
    499499  (*CSC: interactive mode because of dependent types *)
    500   generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
     500  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
    501501  cases (map_partial … transf_partial_variable (prog_vars … p))
    502502  [ #vl #EQ
Note: See TracChangeset for help on using the changeset viewer.