		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

C-char

Fixtype of characters and escape sequences usable in character constants [C:6.4.4.4] [C:A.1.5].

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

Member Tags → Types

:char → c-char-char
:escape → c-char-escape

This corresponds to c-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 single quote, backslash, or new-line.

Subtopics

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