Check if a character value notation denotes values in a set.
(char-val-in-termset-p char-val termset) → yes/no
Function:
(defun char-val-in-termset-p (char-val termset) (declare (xargs :guard (and (char-val-p char-val) (nat-setp termset)))) (char-val-case char-val :sensitive (chars-sensitive-in-termset-p (explode char-val.get) termset) :insensitive (chars-insensitive-in-termset-p (explode char-val.get) termset)))
Theorem:
(defthm booleanp-of-char-val-in-termset-p (b* ((yes/no (char-val-in-termset-p char-val termset))) (booleanp yes/no)) :rule-classes :rewrite)