		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-function-recognizers

Pseudo-termfnp

Recognize pseudo-term-functions, i.e. functions in pseudo-terms.

Signature
(pseudo-termfnp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: pseudo-termfnp

(defun pseudo-termfnp (x)
       (declare (xargs :guard t))
       (let ((__function__ 'pseudo-termfnp))
            (declare (ignorable __function__))
            (or (symbolp x) (pseudo-lambdap x))))

Theorem: booleanp-of-pseudo-termfnp

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

Theorem: pseudo-termfnp-when-symbolp

(defthm pseudo-termfnp-when-symbolp
        (implies (symbolp x)
                 (pseudo-termfnp x)))

Theorem: pseudo-termfnp-when-pseudo-lambdap

(defthm pseudo-termfnp-when-pseudo-lambdap
        (implies (pseudo-lambdap x)
                 (pseudo-termfnp x)))

Theorem: pseudo-termfnp-of-car-when-pseudo-termp

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

Theorem: pseudo-termp-of-cons-when-pseudo-termfnp

(defthm pseudo-termp-of-cons-when-pseudo-termfnp
        (implies (and (pseudo-termfnp fn)
                      (pseudo-term-listp terms)
                      (or (atom fn)
                          (equal (len terms)
                                 (len (lambda-formals fn))))
                      (not (eq fn 'quote)))
                 (pseudo-termp (cons fn terms))))

Subtopics

Pseudo-termfn-listp: Recognize true lists of pseudo-term-functions.