source: src/common/PreIdentifiers.ma @ 2755

Last change on this file since 2755 was 2646, checked in by sacerdot, 7 years ago

A tag was classified as an error message. Fixed.

File size: 769 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 "utilities/binary/positive.ma".
9
10(* identifiers and their generators are tagged to differentiate them, and to
11   provide extra type checking. *)
12
13inductive identifierTag: Type[0] ≝
14   Label : identifierTag
15 | CostTag : identifierTag
16 | RegisterTag : identifierTag
17 | LabelTag : identifierTag
18 | SymbolTag : identifierTag
19 | ASMTag : identifierTag.
20
21inductive identifier (tag:identifierTag) : Type[0] ≝
22  an_identifier : Pos → identifier tag.
Note: See TracBrowser for help on using the repository browser.