lambdap

(in-package "ACL2")

(define lambdap
  (x (wrld plist-worldp-with-formals))
  :returns (yes/no booleanp)
  :parents (std/system/term-function-recognizers)
  :short (topstring "Recognize valid "
    (seetopic "term" "translated")
    " lambda expression,
    i.e. lambda expressions in valid translated terms.")
  :long (topstring-p "This definition mirrors
    the relevant portion of the definition of @(tsee termp).")
  (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))))
  ///
  (defrule lambdap-when-termp
    (implies (and (termp term wrld) (consp term) (consp (car term)))
      (lambdap (car term) wrld)))
  (defrule termp-when-lambdap
    (implies (and (lambdap lambd wrld)
        (term-listp terms wrld)
        (equal (len terms) (len (lambda-formals lambd))))
      (termp (cons lambd terms) wrld)))
  (defrule not-lambdap-of-nil (not (lambdap nil wrld))))