		Search-engine friendly clone of the ACL2 documentation.

Meta-functions

Formal-member

The definition of member for any x on an eqlable-listp constant l.

This definition reposes the question (MEMBER x l) as a set of nested IFs.

Definitions and Theorems

Function: formal-member

(defun formal-member (x l)
 (declare (xargs :guard (and (pseudo-termp x)
                             (eqlable-listp l))))
 (cond
  ((endp l) *nil*)
  (t (cons 'if
           (cons (cons 'eql
                       (cons x
                             (cons (cons 'quote (cons (car l) 'nil))
                                   'nil)))
                 (cons (cons 'quote (cons l 'nil))
                       (cons (formal-member x (cdr l))
                             'nil)))))))