termfn-listp

(in-package "ACL2")

(deflist termfn-listp
  (x wrld)
  :parents (std/system/term-function-recognizers termfnp)
  :short (topstring "Recognize true lists of "
    (seetopic "termfnp" "translated term functions")
    ".")
  :long (topstring-p "We would need stronger world assumptions for @(':elementp-of-nil nil'),
    so with the current weaker world assumptions we leave the default,
    i.e. @(':elementp-of-nil :unknown').")
  :guard (plist-worldp-with-formals wrld)
  (termfnp x wrld)
  :true-listp t)