|
Last change
on this file since 2989 was
2646,
checked in by sacerdot, 8 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 | |
|---|
| 7 | include "basics/types.ma". |
|---|
| 8 | include "utilities/binary/positive.ma". |
|---|
| 9 | |
|---|
| 10 | (* identifiers and their generators are tagged to differentiate them, and to |
|---|
| 11 | provide extra type checking. *) |
|---|
| 12 | |
|---|
| 13 | inductive identifierTag: Type[0] ≝ |
|---|
| 14 | Label : identifierTag |
|---|
| 15 | | CostTag : identifierTag |
|---|
| 16 | | RegisterTag : identifierTag |
|---|
| 17 | | LabelTag : identifierTag |
|---|
| 18 | | SymbolTag : identifierTag |
|---|
| 19 | | ASMTag : identifierTag. |
|---|
| 20 | |
|---|
| 21 | inductive identifier (tag:identifierTag) : Type[0] ≝ |
|---|
| 22 | an_identifier : Pos → identifier tag. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
