Exec-character-set
Execution character set.
The execution character set is analogous to the source character set
except that it has a few additional basic characters [C17:5.2.1].
We formalize the execution characters
analogously to the source characters,
i.e. as a constrained predicate
with an injection from the ASCII basic ones
and an injection to numbers.
These numbers are not the values of the execution characters,
which will be formalized elsewhere;
the significance of these number is limited to our ACL2 formalization.
See source-character-set for details.
Subtopics
- Exec-char-recognizer+fixer+mappings+fixtype
- Constrained recognizer and fixer and mappings, and fixtype,
for the execution character set.
- Ascii-basic-exec-char
- Fixtype for ascii-basic-exec-charp.
- Ascii-basic-exec-charp
- Recognize the ACL2 ASCII characters that correspond to
the members of the basic execution character set in C.
- Ascii-to-exec-char-number
- Number of the basic execution character
corresponding to an ASCII character.
- Ascii-basic-exec-char-fix
- Fixer for ascii-basic-exec-char.
- Ext-exec-charp
- Recognize the extended execution characters.
- Basic-exec-charp
- Recognize the basic execution characters.
