(vl-stringtoken-p x) is a defaggregate of the following fields.
etext — The characters that gave rise to this string literal from the
Verilog source. Note that this text is "verbatim" and, as a
consequence, character sequences like \n will not have been
converted into newlines, etc. Invariant (and (vl-echarlist-p etext) (consp etext) (true-listp etext)).
expansion — An ordinary ACL2 string object that holds the "expanded"
version of the string literal. That is, character sequences
like \n in the etext become real newline characters
in the expansion. Invariant (stringp expansion).
Source link: vl-stringtoken-p
The expansion is carried out per Table 3-1, on page 14 of the
Verilog-2005 standard. BOZO is that still valid for SystemVerilog?
