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