		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-function-recognizers

Lambdap

Recognize valid translated lambda expression, i.e. lambda expressions in valid translated terms.

Signature
(lambdap x wrld) → yes/no
Arguments: wrld — Guard (plist-worldp-with-formals wrld).
Returns: yes/no — Type (booleanp yes/no).

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

Definitions and Theorems

Function: lambdap

(defun lambdap (x wrld)
  (declare (xargs :guard (plist-worldp-with-formals wrld)))
  (let ((__function__ 'lambdap))
    (declare (ignorable __function__))
    (and (true-listp x)
         (= (len x) 3)
         (eq (first x) 'lambda)
         (arglistp (second x))
         (termp (third x) wrld)
         (null (set-difference-eq (all-vars (third x))
                                  (second x))))))

Theorem: booleanp-of-lambdap

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

Theorem: lambdap-when-termp

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

Theorem: termp-when-lambdap

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

Theorem: not-lambdap-of-nil

(defthm not-lambdap-of-nil
  (not (lambdap nil wrld)))

Subtopics

Lambda-listp: Recognize true lists of translated lambda expressions.