		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-function-recognizers

Termfnp

Recognize valid translated term functions, i.e. functions in valid translated terms.

Signature
(termfnp x wrld) → yes/no
Arguments: wrld — Guard (plist-worldp-with-formals wrld).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: termfnp

(defun termfnp (x wrld)
  (declare (xargs :guard (plist-worldp-with-formals wrld)))
  (let ((__function__ 'termfnp))
    (declare (ignorable __function__))
    (or (and (symbolp x)
             (function-symbolp x wrld))
        (lambdap x wrld))))

Theorem: booleanp-of-termfnp

(defthm booleanp-of-termfnp
  (b* ((yes/no (termfnp x wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: termfnp-when-termp

(defthm termfnp-when-termp
  (implies (and (termp term wrld)
                (consp term)
                (consp (car term)))
           (termfnp (car term) wrld)))

Theorem: termp-when-termfnp

(defthm 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)))

Subtopics

Termfn-listp: Recognize true lists of translated term functions.