source: src/common/Registers.ma @ 2783

Last change on this file since 2783 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 422 bytes
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4(*include "ASM/BitVectorTrie.ma".*)
5include "common/Identifiers.ma".
6(*include "ASM/I8051.ma".*)
7include "common/Order.ma".
8
9definition register ≝ identifier RegisterTag.
10
11definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
12
13definition register_env ≝ identifier_map RegisterTag.
14
15(*
16axiom register_ord: register → register → order.
17*)
Note: See TracBrowser for help on using the repository browser.