Leo symbols.
Here we capture the Leo symbols in ACL2. Since they all consist of ASCII characters, we can use ACL2 strings for this purpose.