pseudo-lambdap

(in-package "ACL2")

(define pseudo-lambdap
  (x)
  :returns (yes/no booleanp)
  :parents (std/system/term-function-recognizers)
  :short (topstring "Recognize pseudo-lambda-expressions,
    i.e. lambda expressions in "
    (seetopic "pseudo-termp" "pseudo-terms")
    ".")
  :long (topstring-p "This definition mirrors
    the relevant portion of the definition of @(tsee pseudo-termp).")
  (and (true-listp x)
    (= (len x) 3)
    (eq (first x) 'lambda)
    (symbol-listp (second x))
    (pseudo-termp (third x)))
  ///
  (defrule pseudo-lambdap-of-car-when-pseudo-termp
    (implies (and (pseudo-termp term) (consp term) (consp (car term)))
      (pseudo-lambdap (car term))))
  (defrule 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)))))