		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Char-insensitive-in-termset-p

Check if the code of a character, as well as the codes of its uppercase or lowercase counterparts, are in a set.

Signature
(char-insensitive-in-termset-p char termset) → yes/no
Arguments: char — Guard (characterp char).; termset — Guard (nat-setp termset).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: char-insensitive-in-termset-p

(defun char-insensitive-in-termset-p (char termset)
  (declare (xargs :guard (and (characterp char)
                              (nat-setp termset))))
  (and (in (char-code char) termset)
       (in (char-code (upcase-char char))
           termset)
       (in (char-code (downcase-char char))
           termset)))

Theorem: booleanp-of-char-insensitive-in-termset-p

(defthm booleanp-of-char-insensitive-in-termset-p
  (b* ((yes/no (char-insensitive-in-termset-p char termset)))
    (booleanp yes/no))
  :rule-classes :rewrite)