Identifiers
Leo identifiers.
In Leo, identifiers are non-empty sequences of ASCII characters,
starting with a letter
and containing only letters, digits, and underscore.
They must also be distinct from
all the keywords and the boolean literals.
They must also not be, or start with, aleo1.
Since the ASCII characters are
a subset of ACL2's ISO 8851-1 characters,
it is adequate to represent Leo identifiers
as sequences of ACL2 characters, i.e. as ACL2 strings.
Subtopics
- Identifier
- Fixtype of Leo identifiers.
- Identifier-option
- Fixtype of optional Leo identifiers.
- Programid
- Fixtype of program IDs.
- Locator
- Fixtype of locators.
- Identifier-grammar-chars-p
- Check if a list of characters forms a Leo identifier
according to the ABNF grammar rule for identifiers.
- Identifier-option-result
- Fixtype of errors and optional Leo identifiers.
- Programid-result
- Fixtype of errors and Leo program IDs.
- Locator-result
- Fixtype of errors and Leo locators.
- Identifier-result
- Fixtype of errors and Leo identifiers.
- Identifier-list-result
- Fixtype of errors and lists of Leo identifiers.
- Identifier-string-p
- Check if a string is a valid Leo identifier.
- Identifier-set
- Fixtype of osets of Leo identifiers.
- Identifier-list
- Fixtype of lists of Leo identifiers.
