Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1515 r2176  
    2424 pointer → label → Σp:pointer. ptype p = Code ≝
    2525 λoldpc,l.
    26   mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
     26  mk_pointer
     27   (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))).
    2828// qed.
    2929
Note: See TracChangeset for help on using the changeset viewer.