pseudo-termfn-listp

(in-package "ACL2")

(deflist pseudo-termfn-listp
  (x)
  :parents (std/system/term-function-recognizers pseudo-termfnp)
  :short (topstring "Recognize true lists of "
    (seetopic "pseudo-termfnp" "pseudo-term-functions")
    ".")
  (pseudo-termfnp x)
  :true-listp t
  :elementp-of-nil t)