Changeset 1610
- Timestamp:
- Dec 14, 2011, 3:33:57 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r1608 r1610 53 53 | elim init 54 54 [ % // 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 ] 56 56 ] qed. 57 57 58 58 definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝ 59 59 λ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 …)) ] 62 62 qed. 63 63 … … 77 77 list (ident × (fundef internal_function)) → 78 78 list (ident × (fundef internal_function)) ≝ 79 λid,s. match s with [ dps H ⇒79 λid,s. match s with [ mk_Sig s H ⇒ 80 80 map ?? 81 81 (λidf.
Note: See TracChangeset
for help on using the changeset viewer.