CHAR-EQUAL

character equality without regard to case
Major Section:  ACL2-BUILT-INS

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 case.

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.

To see the ACL2 definition of this function, see pf.