Changeset 1395 for src/common/GenMem.ma
- Timestamp:
- Oct 17, 2011, 5:41:44 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/GenMem.ma
r1213 r1395 126 126 qed. 127 127 128 definition alloc : ∀content. mem content → Z → Z → region → mem content × block≝128 definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝ 129 129 λcontent,m,lo,hi,r. 130 130 let b ≝ mk_block r (nextblock … m) in … … 136 136 (succ_nextblock_pos … m), 137 137 b〉. 138 % qed. 138 139 139 140 (* Freeing a block. Return the updated memory state where the given
Note: See TracChangeset
for help on using the changeset viewer.