Changeset 2793 for src/Cminor
- Timestamp:
- Mar 6, 2013, 7:23:42 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r2624 r2793 45 45 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝ 46 46 λid,r,init. 47 \snd (fold r??48 (λ datum,os.47 \snd (foldl ?? 48 (λos,datum. 49 49 let 〈off,s〉 ≝ os in 50 50 〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉) 51 51 〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init). 52 52 [ % /3/ 53 | elim init 54 [ % /3/ 55 | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair 53 | cut (stmt_inv St_skip) [ % /3/ ] 54 generalize in match St_skip; 55 generalize in match 0; 56 elim init 57 [ #off #s #H @H 58 | #h #t #IH #off #s #H whd in ⊢ (?(???%)); @breakup_pair @IH 56 59 % 57 60 [ /3/ 58 | % [ @(pi2 … (init_datum …)) | @ IH ]61 | % [ @(pi2 … (init_datum …)) | @H ] 59 62 ] 63 ] 60 64 ] qed. 61 65
Note: See TracChangeset
for help on using the changeset viewer.