(* Basic identifier definition.  This is done separately from the rest of the
   definitions for identifiers so that error messages can use identifiers
   and the other definitions can use the error monad (without having to
   parametrise the monad by the type of error messages). *)

include "basics/types.ma".
include "ASM/String.ma".
include "ASM/Arithmetic.ma".

(* identifiers and their generators are tagged to differentiate them, and to
   provide extra type checking. *)

inductive identifier (tag:String) : Type[0] ≝
  an_identifier : Word → identifier tag.