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