source: src/common/Registers.ma @ 737

Last change on this file since 737 was 736, checked in by campbell, 9 years ago

Extra type safety for identifiers.

File size: 358 bytes
RevLine 
[639]1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5
[726]6include "ASM/BitVectorTrie.ma".
[736]7include "common/Identifiers.ma".
[639]8
[736]9axiom RegisterTag : String.
[639]10
[736]11definition register ≝ Identifier RegisterTag.
[639]12
[736]13definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
[639]14
[736]15definition register_env ≝ IdentifierMap RegisterTag.
Note: See TracBrowser for help on using the repository browser.