		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

S-char

Fixtype of characters and escape sequences usable in string literals [C:6.4.5] [C:A.1.6].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:char → s-char-char
:escape → s-char-escape

This corresponds to s-char in the grammar in [C].

As explained in abstract-syntax, the natural numbers represent Unicode code points. We do not capture the restriction that the characters cannot be double quote, backslash, or new-line.

Subtopics

S-char-case: Case macro for the different kinds of s-char structures.
S-char-fix: Fixing function for s-char structures.
S-char-equiv: Basic equivalence relation for s-char structures.
S-char-p: Recognizer for s-char structures.
S-char-escape
S-char-char
S-char-kind: Get the kind (tag) of a s-char structure.