(* NB: this is essentially the same as Graphs! *)

include "basics/types.ma".

include "ASM/BitVectorTrie.ma".
include "common/Identifiers.ma".

axiom RegisterTag : String.

definition register ≝ identifier RegisterTag.

definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.

definition register_env ≝ identifier_map RegisterTag.