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/Cminor/initialisation.ma

    r1401 r1516  
    5555| elim init
    5656  [ % //
    57   | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
     57  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
    5858] qed.
    5959
     
    6666lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
    6767#s elim s //
    68 [ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     68[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6969  >(IH1 H1) >(IH2 H2) @refl
    70 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     70| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    7171  >(IH1 H1) >(IH2 H2) @refl
    7272| #s #IH * * #_ #_ #H @(IH H)
     
    103103  ]
    104104  ]
    105 | whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
     105| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?); >(no_labels … H) @(f_inv f)
    106106] qed.
    107107
Note: See TracChangeset for help on using the changeset viewer.