(* 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 "utilities/binary/positive.ma". (* identifiers and their generators are tagged to differentiate them, and to provide extra type checking. *) inductive identifier (tag:String) : Type[0] ≝ an_identifier : Pos → identifier tag.