Ignore:
Timestamp:
Mar 25, 2011, 6:37:49 PM (9 years ago)
Author:
campbell
Message:

Start of way to import RTLabs from prototype compiler.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Registers.ma

    r702 r710  
    1515record register_generation : Type[0] ≝ { reg_next : register }.
    1616
     17definition register_gen_new : register_generation ≝ mk_register_generation one.
     18
    1719definition register_new : register_generation → register × register_generation ≝
    1820λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
Note: See TracChangeset for help on using the changeset viewer.