		Search-engine friendly clone of the ACL2 documentation.

Undocumented

List-notin

(list-notin x set) recognizes lists where every element satisfies not.

Signature
(list-notin 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: list-notin

(defun list-notin (x set)
  (declare (xargs :guard (and (true-listp x) (setp set))))
  (let ((acl2::__function__ 'list-notin))
    (declare (ignorable acl2::__function__))
    (if (consp x)
        (and (not (in (car x) set))
             (list-notin (cdr x) set))
      t)))

Theorem: list-notin-of-sfix-2

(defthm list-notin-of-sfix-2
  (equal (list-notin list (sfix set))
         (list-notin list set)))

Subtopics

List-notin-basics: Basic theorems about list-notin, generated by std::deflist.