Changeset 2793 for src


Ignore:
Timestamp:
Mar 6, 2013, 7:23:42 PM (7 years ago)
Author:
campbell
Message:

Oops, gave fields wrong order during initialisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2624 r2793  
    4545definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
    4646λid,r,init.
    47 \snd (foldr ??
    48   (λdatum,os.
     47\snd (foldl ??
     48  (λos,datum.
    4949   let 〈off,s〉 ≝ os in
    5050     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    5151  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    5252[ % /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
    5659    %
    5760    [ /3/
    58     | % [ @(pi2 … (init_datum …)) | @IH ]
     61    | % [ @(pi2 … (init_datum …)) | @H ]
    5962    ]
     63  ]
    6064] qed.
    6165
Note: See TracChangeset for help on using the changeset viewer.