Recognize ASCII letters.
The built-in alpha-char-p
has a guard requiring characters that are standard.
In contrast, this recognizer has guard
(defun letter-char-p (x) (declare (xargs :guard t)) (and (characterp x) (b* ((code (char-code x))) (or (and (<= (char-code #\A) code) (<= code (char-code #\Z))) (and (<= (char-code #\a) code) (<= code (char-code #\z)))))))
(defthm booleanp-of-letter-char-p (booleanp (letter-char-p x)) :rule-classes :type-prescription)
(defthm characterp-when-letter-char-p (implies (letter-char-p x) (characterp x)) :rule-classes :compound-recognizer)