		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Chars-sensitive-in-termset-p

Lift char-sensitive-in-termset-p to lists.

Signature
(chars-sensitive-in-termset-p x termset) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: chars-sensitive-in-termset-p

(defun chars-sensitive-in-termset-p (x termset)
  (declare (xargs :guard (and (character-listp x)
                              (nat-setp termset))))
  (let ((__function__ 'chars-sensitive-in-termset-p))
    (declare (ignorable __function__))
    (if (consp x)
        (and (char-sensitive-in-termset-p (car x)
                                          termset)
             (chars-sensitive-in-termset-p (cdr x)
                                           termset))
      t)))

Subtopics

Chars-sensitive-in-termset-p-basics: Basic theorems about chars-sensitive-in-termset-p, generated by std::deflist.