		Search-engine friendly clone of the ACL2 documentation.

Oset-utilities

List-in

Lift in to lists.

Signature
(list-in 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-in

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

Theorem: list-in-of-sfix-2

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

Subtopics

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