source: src/common/Registers.ma @ 1049

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

more stuff added

File size: 585 bytes
RevLine 
[639]1
2(* NB: this is essentially the same as Graphs! *)
3
[726]4include "ASM/BitVectorTrie.ma".
[736]5include "common/Identifiers.ma".
[757]6include "ASM/I8051.ma".
[1049]7include "common/Order.ma".
[639]8
[736]9axiom RegisterTag : String.
[639]10
[738]11definition register ≝ identifier RegisterTag.
[639]12
[736]13definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
[639]14
[738]15definition register_env ≝ identifier_map RegisterTag.
[757]16
[1049]17axiom register_ord: register → register → order.
18
[757]19(* dpm: fix the Register/register mismatch *)
[777]20axiom Register_of_register: register → Register.
21axiom register_of_Register: Register → register.
Note: See TracBrowser for help on using the repository browser.