• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/system
        • Fresh-logical-name-with-$s-suffix
        • Irrelevant-formals-info
        • Std/system/function-queries
        • Std/system/term-queries
        • Std/system/term-transformations
        • Std/system/enhanced-utilities
        • Install-not-normalized-event-lst
        • Install-not-normalized-event
        • Std/system/term-function-recognizers
          • Pseudo-termfnp
            • Pseudo-termfn-listp
          • Pseudo-lambdap
          • Lambdap
          • Termfnp
          • Pseudo-lambda-listp
          • Pseudo-termfn-listp
          • Termfn-listp
          • Lambda-listp
        • Pseudo-tests-and-call-listp
        • Genvar$
        • Std/system/event-name-queries
        • Maybe-pseudo-event-formp
        • Add-suffix-to-fn-or-const
        • Chk-irrelevant-formals-ok
        • Std/system/good-atom-listp
        • Pseudo-tests-and-callp
        • Table-alist+
        • Add-suffix-to-fn-or-const-lst
        • Known-packages+
        • Add-suffix-to-fn-lst
        • Unquote-term
        • Event-landmark-names
        • Add-suffix-lst
        • Std/system/theorem-queries
        • Unquote-term-list
        • Std/system/macro-queries
        • Pseudo-event-landmark-listp
        • Pseudo-command-landmark-listp
        • Install-not-normalized$
        • Rune-disabledp
        • Known-packages
        • Std/system/partition-rest-and-keyword-args
        • Rune-enabledp
        • Included-books
        • Std/system/pseudo-event-formp
        • Std/system/plist-worldp-with-formals
        • Std/system/w
        • Std/system/geprops
        • Std/system/arglistp
        • Std/system-extensions
        • Std/system/constant-queries
      • Std/basic
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
      • Std-extensions
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • 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.