		Search-engine friendly clone of the ACL2 documentation.

Character-literals

Char-literal

Fixtype of character literals.

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

Member Tags → Types

:char → char-literal-char
:escape → char-literal-escape

According to the grammar rule for character-literal [JLS14:3.10.4], a character literal is either a single-character (see unicode-charlit-char) or an escape sequence (see escape-sequence), between single quotes. Abstractly, but without losing any information, we leave the surrounding single quotes implicit, and define character literals via a tagged sum.

The set of values of this fixtype should be isomorphic to the set of strings (or parse trees) defined by the Java grammar rule character-literal. This remains to be proved formally.

Subtopics

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