Q-char-list
Fixtype of lists of characters usable in
header names between double quotes [C17:6.4.7] [C17:A.1.8].
Characters usable in header names between double quotes
are defined in q-char.
Subtopics
- Q-char-list-fix
- (q-char-list-fix x) is a usual ACL2::fty list fixing function.
- Q-char-list-equiv
- Basic equivalence relation for q-char-list structures.
- Q-char-listp
- (q-char-listp x) recognizes lists where every element satisfies q-char-p.
