		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-function-recognizers

Pseudo-lambdap

Recognize pseudo-lambda-expressions, i.e. lambda expressions in pseudo-terms.

Signature
(pseudo-lambdap x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

This definition mirrors the relevant portion of the definition of pseudo-termp.

Definitions and Theorems

Function: pseudo-lambdap

(defun pseudo-lambdap (x)
  (declare (xargs :guard t))
  (let ((__function__ 'pseudo-lambdap))
    (declare (ignorable __function__))
    (and (true-listp x)
         (= (len x) 3)
         (eq (first x) 'lambda)
         (symbol-listp (second x))
         (pseudo-termp (third x)))))

Theorem: booleanp-of-pseudo-lambdap

(defthm booleanp-of-pseudo-lambdap
  (b* ((yes/no (pseudo-lambdap x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-lambdap-of-car-when-pseudo-termp

(defthm pseudo-lambdap-of-car-when-pseudo-termp
  (implies (and (pseudo-termp term)
                (consp term)
                (consp (car term)))
           (pseudo-lambdap (car term))))

Theorem: pseudo-termp-of-cons-when-pseudo-lambdap

(defthm pseudo-termp-of-cons-when-pseudo-lambdap
  (implies (and (pseudo-lambdap lambd)
                (pseudo-term-listp terms)
                (equal (len terms)
                       (len (lambda-formals lambd))))
           (pseudo-termp (cons lambd terms))))

Subtopics

Pseudo-lambda-listp: Recognize true lists of pseudo-lambda-expressions.