		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Plain-string

Fixtype of plain strings.

This is a product type introduced by fty::defprod.

Fields

content — string-element-list
double-quote-p — booleanp

These are used as literals; they are the regular, non-hex strings. We call them `plain' to clearly distinguish them from hex strings.

We represent a plain string as a list of elements, plus a flag saying whether the surrounding quotes are double or not (i.e. single). This captures the full concrete syntax information.

Subtopics

Plain-string-fix: Fixing function for plain-string structures.
Plain-string-equiv: Basic equivalence relation for plain-string structures.
Make-plain-string: Basic constructor macro for plain-string structures.
Plain-string->double-quote-p: Get the double-quote-p field from a plain-string.
Plain-string->content: Get the content field from a plain-string.
Change-plain-string: Modifying constructor for plain-string structures.
Plain-stringp: Recognizer for plain-string structures.