source: Deliverables/D3.3/id-lookup-branch/common/

Last change on this file was 797, checked in by campbell, 9 years ago

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 572 bytes
2(* Basic identifier definition.  This is done separately from the rest of the
3   definitions for identifiers so that error messages can use identifiers
4   and the other definitions can use the error monad (without having to
5   parametrise the monad by the type of error messages). *)
7include "basics/".
8include "ASM/".
9include "ASM/".
11(* identifiers and their generators are tagged to differentiate them, and to
12   provide extra type checking. *)
14inductive identifier (tag:String) : Type[0] ≝
15  an_identifier : Word → identifier tag.
Note: See TracBrowser for help on using the repository browser.