source: src/common/PreIdentifiers.ma @ 1480

Last change on this file since 1480 was 797, checked in by campbell, 10 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
Line 
1
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). *)
6
7include "basics/types.ma".
8include "ASM/String.ma".
9include "ASM/Arithmetic.ma".
10
11(* identifiers and their generators are tagged to differentiate them, and to
12   provide extra type checking. *)
13
14inductive identifier (tag:String) : Type[0] ≝
15  an_identifier : Word → identifier tag.
Note: See TracBrowser for help on using the repository browser.