lambda-listp

(in-package "ACL2")

(deflist lambda-listp
  (x wrld)
  :parents (std/system/term-function-recognizers lambdap)
  :short (topstring "Recognize true lists of "
    (seetopic "lambdap" "translated lambda expressions")
    ".")
  :guard (plist-worldp-with-formals wrld)
  (lambdap x wrld)
  :true-listp t
  :elementp-of-nil nil)