source: src/common/Registers.ma @ 764

Last change on this file since 764 was 757, checked in by mulligan, 9 years ago

Lots more fixing to get both front and backends using same conventions and types.

File size: 481 bytes
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5
6include "ASM/BitVectorTrie.ma".
7include "common/Identifiers.ma".
8include "ASM/I8051.ma".
9
10axiom RegisterTag : String.
11
12definition register ≝ identifier RegisterTag.
13
14definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
15
16definition register_env ≝ identifier_map RegisterTag.
17
18(* dpm: fix the Register/register mismatch *)
19axiom Register_of_register: register → Register.
Note: See TracBrowser for help on using the repository browser.