Unicode characters.
Leo is written in Unicode. Here we introduce a notion of Unicode characters, used to formalize the concrete syntax of Leo.
In the future, ideally we should make use of a more general ACL2 library for Unicode, of which the community books have an initial version (which could and should be expanded).