Character equality without regard to case
For characters x and y, (char-equal x y) is
true if and only if x and y are the same except perhaps for their
The guard on char-equal requires that its arguments are both
standard characters (see standard-char-p).
Char-equal is a Common Lisp function. See any Common Lisp
documentation for more information.
(defun char-equal (x y)
(declare (xargs :guard (and (characterp x)
(eql (char-downcase x)