		Search-engine friendly clone of the ACL2 documentation.

Charset-p

Chars-in-charset-p

(chars-in-charset-p x set) recognizes lists of characters x where every character is a member of the charset-p set.

Signature
(chars-in-charset-p x set) → 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-in-charset-p

(defun chars-in-charset-p (x set)
  (declare (xargs :guard (and (character-listp x)
                              (charset-p set))))
  (let ((acl2::__function__ 'chars-in-charset-p))
    (declare (ignorable acl2::__function__))
    (if (consp x)
        (and (char-in-charset-p (car x) set)
             (chars-in-charset-p (cdr x) set))
      t)))

Subtopics

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