In the abstract syntax,
we use character strings
for the bracketed prose described by the rule prose-val in [RFC:4].
We abstract away the restriction
that the prose include only certain characters
(which all are ACL2 characters).
This restriction is captured by the notion of well-formed prose value notations.
