		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Char-sensitive-in-termset-p

Check if the code of a character is in a set.

Signature
(char-sensitive-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-sensitive-in-termset-p

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

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

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