		Search-engine friendly clone of the ACL2 documentation.

String-literals

String-literal-char

Fixtype of characters for string literals.

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

Member Tags → Types

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

According to the grammar rule for string-character [JLS14:3.10.5], a character for a string literal is either a Unicode input character with some exceptions (see unicode-stringlit-char) or an escape sequence (see escape-sequence).

We prefer the nomenclature `string literal character', on which this type name is based, to the nomenclature `string character' suggested by the grammar.

Subtopics

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