C-char-list
Fixtype of lists of characters and escape sequences
usable in character constants [C:6.4.4.4] [C:A.1.5].
Characters and escape sequences usable in character constants
are defined in c-char.
Subtopics
- C-char-list-fix
- (c-char-list-fix x) is a usual ACL2::fty list fixing function.
- C-char-list-equiv
- Basic equivalence relation for c-char-list structures.
- C-char-listp
- (c-char-listp x) recognizes lists where every element satisfies c-char-p.