Recursion and Induction: Characters
We will not use character objects in this document. In case you come across such an object in your exploration of ACL2, some characters are #\a, #\A, #\Newline and #\Space. It is actually possible in ACL2 to “construct” and “deconstruct” characters in terms of naturals. For example, one can construct #\A from 65, the ASCII code for uppercase `A'.
(Maybe explore <<characters>>?)