		Search-engine friendly clone of the ACL2 documentation.

Pseudo-lambda

Pseudo-lambda-p

Signature
(pseudo-lambda-p x) → *

Definitions and Theorems

Function: pseudo-lambda-p

(defun pseudo-lambda-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'pseudo-lambda-p))
    (declare (ignorable __function__))
    (and (true-listp x)
         (eql (len x) 3)
         (eq (car x) 'lambda)
         (symbol-listp (cadr x))
         (pseudo-termp (caddr x)))))

Theorem: pseudo-lambda-p-compound-recognizer

(defthm pseudo-lambda-p-compound-recognizer
  (implies (pseudo-lambda-p x)
           (and (consp x) (true-listp x)))
  :rule-classes :compound-recognizer)