Ignore:
Timestamp:
Sep 16, 2011, 5:15:35 PM (9 years ago)
Author:
mulligan
Message:

changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/adt/register_table.ma

    r1211 r1223  
    11include "ASM/I8051.ma".
    22include "common/Registers.ma".
    3 include "utilities/adt/ordering.ma".
    43include "utilities/adt/set_adt.ma".
    54
    65definition vertex ≝ nat. (* XXX: int in o'caml *)
    76
     7(*
    88axiom Register_ordered: ordered Register.
    99axiom register_ordered: ordered register.
    1010axiom vertex_ordered: ordered vertex.
     11*)
    1112
    1213axiom register_table: Type[0].
    1314 
    1415axiom rt_empty : register_table.
     16
     17axiom rt_insert: vertex → set Register → register_table → register_table.
    1518 
    1619axiom rt_forward : vertex → register_table → set Register.
Note: See TracChangeset for help on using the changeset viewer.