Char-val
Fixtype of character value notations.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :sensitive → char-val-sensitive
- :insensitive → char-val-insensitive
In the abstract syntax,
we use character strings
for the literal text strings described in [RFC:2.3]
and by the rule char-val (and sub-rules) in [RFC:4].
We tag strings with an indication of their case sensitivity,
corresponding to the %s and %i notations.
We also keep information about whether case-insensitive strings
have an explicit %i prefix or not.
Even though this is irrelevant semantically,
we prefer to retain that information from the concrete syntax
(e.g. for better pretty-printing),
instead of abstracting it away.
We abstract away the restriction
that quoted strings include only certain characters
(which all are ACL2 characters).
This restriction is captured by the notion of well-formed character value notations.
Subtopics
- Char-val-case
- Case macro for the different kinds of char-val structures.
- Char-val-fix
- Fixing function for char-val structures.
- Char-val-equiv
- Basic equivalence relation for char-val structures.
- Char-val-p
- Recognizer for char-val structures.
- Char-val-insensitive
- Char-val-sensitive
- Char-val-kind
- Get the kind (tag) of a char-val structure.
