termfnp

(in-package "ACL2")

(define termfnp
  (x (wrld plist-worldp-with-formals))
  :returns (yes/no booleanp)
  :parents (std/system/term-function-recognizers)
  :short (topstring "Recognize valid "
    (seetopic "term" "translated")
    " term functions,
    i.e. functions in valid translated terms.")
  (or (and (symbolp x) (function-symbolp x wrld))
    (lambdap x wrld))
  ///
  (defrule termfnp-when-termp
    (implies (and (termp term wrld) (consp term) (consp (car term)))
      (termfnp (car term) wrld)))
  (defrule termp-when-termfnp
    (implies (and (termfnp fn wrld)
        (term-listp terms wrld)
        (equal (len terms) (arity fn wrld))
        (not (eq fn 'quote)))
      (termp (cons fn terms) wrld))
    :enable (arity lambdap)))