source: src/common/PreIdentifiers.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 743 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
20inductive identifier (tag:identifierTag) : Type[0] ≝
21  an_identifier : Pos → identifier tag.
Note: See TracBrowser for help on using the repository browser.