source: src/common/Registers.ma @ 753

Last change on this file since 753 was 738, checked in by campbell, 9 years ago

Use lower case names for identifiers for consistency with CompCert? derived code
and to prevent confusion with the back-end equivalents until they're all merged.

File size: 360 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".
8
9axiom RegisterTag : String.
10
11definition register ≝ identifier RegisterTag.
12
13definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
14
15definition register_env ≝ identifier_map RegisterTag.
Note: See TracBrowser for help on using the repository browser.