Changeset 1610 for src/Cminor


Ignore:
Timestamp:
Dec 14, 2011, 3:33:57 PM (8 years ago)
Author:
sacerdot
Message:

Ported to new lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1608 r1610  
    5353| elim init
    5454  [ % //
    55   | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 ? stmt_inv) ] | @IH ]
     55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 … (init_datum …)) ] | @IH ]
    5656] qed.
    5757
    5858definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5959λvars. foldr ? (Σs:stmt. stmt_inv s)
    60   (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    61 % [ % [ % // | @(pi2 ? stmt_inv) ] | @(pi2 ? stmt_inv) ]
     60  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     61% [ % [ % // | @(pi2 … s) ] | @(pi2 … (init_var …)) ]
    6262qed.
    6363
     
    7777                              list (ident × (fundef internal_function)) →
    7878                              list (ident × (fundef internal_function)) ≝
    79 λid,s. match s with [ dp s H ⇒
     79λid,s. match s with [ mk_Sig s H ⇒
    8080  map ??
    8181    (λidf.
Note: See TracChangeset for help on using the changeset viewer.