source: src/common/Registers.ma @ 738

Last change on this file since 738 was 738, checked in by campbell, 10 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.