Recursion and Induction: Strings
Strings in our subset of ACL2 are written as sequences of ASCII characters between successive string quotes. For example, here is a string: "Hello, World!". For the purposes of this document, we will treat strings as atomic objects, though it is actually possible to construct and deconstruct them in terms of lists of character objects.
(Maybe explore <<strings>>?)