Changeset 745 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Apr 8, 2011, 10:15:30 AM (9 years ago)
Author:
mulligan
Message:

Changes from yesterday. Slowly implementing the functorized imperative code from ERTL :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r735 r745  
    44include "common/Graphs.ma".
    55
    6 definition AbstractRegister ≝ nat.
     6inductive AbstractRegister: Type[0] ≝
     7  mkAbstractRegister: Word → AbstractRegister.
     8
    79definition AbstractRegisters ≝ list AbstractRegister.
    810
Note: See TracChangeset for help on using the changeset viewer.