		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.