Changeset 2105 for src/common/GenMem.ma


Ignore:
Timestamp:
Jun 21, 2012, 5:21:04 PM (8 years ago)
Author:
campbell
Message:

Show some results about globalenvs and program transformations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r1993 r2105  
    121121qed.
    122122
    123 definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝
    124   λm,lo,hi,r.
     123let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r ≝
    125124  let b ≝ mk_block r (nextblock … m) in
    126125  〈mk_mem
Note: See TracChangeset for help on using the changeset viewer.