String-literal
Fixtype of string literals.
According to the grammar rule for string-literal [JLS14:3.10.5],
a string literal consists of zero or more string-characters
(which we formalize via string-literal-char)
between double quotes.
Abstractly, but without losing any information,
we leave the surrounding double quotes implicit,
and define string literals as lists.
The set of values of this fixtype should be isomorphic to
the set of strings (or parse trees) defined by
the Java grammar rule string-literal.
This remains to be proved formally.
Subtopics
- String-literal-fix
- (string-literal-fix x) is a usual ACL2::fty list fixing function.
- String-literal-equiv
- Basic equivalence relation for string-literal structures.
- String-literalp
- (string-literalp x) recognizes lists where every element satisfies string-literal-char-p.
