• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
      • 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
        • Install-not-normalized-event-lst
        • Std/system/term-function-recognizers
        • Genvar$
        • Std/system/event-name-queries
          • Logic-function-namep
          • Function-namep
            • Theorem-symbolp
            • Macro-symbolp
            • Logical-name-listp
            • Constant-symbolp
            • Theorem-symbol-listp
            • Theorem-name-listp
            • Macro-symbol-listp
            • Macro-name-listp
            • Function-symbol-listp
            • Function-name-listp
            • Theorem-namep
            • Macro-namep
            • Constant-namep
            • Fresh-namep
            • Std/system/function-symbolp
          • Pseudo-tests-and-call-listp
          • Maybe-pseudo-event-formp
          • Add-suffix-to-fn-or-const
          • Chk-irrelevant-formals-ok
          • Table-alist+
          • Pseudo-tests-and-callp
          • 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-command-landmark-listp
          • Install-not-normalized$
          • Pseudo-event-landmark-listp
          • Known-packages
          • Std/system/partition-rest-and-keyword-args
          • Rune-enabledp
          • Rune-disabledp
          • Included-books
          • Std/system/pseudo-event-formp
          • Std/system/plist-worldp-with-formals
          • Std/system/w
          • Std/system/geprops
          • Std/system/arglistp
          • Std/system/constant-queries
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Community
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Std/system/event-name-queries

    Function-namep

    Recognize symbols that name functions.

    Signature
    (function-namep x wrld) → yes/no
    Arguments
    wrld — Guard (plist-worldp wrld).
    Returns
    yes/no — Type (booleanp yes/no).

    This function is enabled because it is meant as an abbreviation. Theorems triggered by this function should be generally avoided.

    Definitions and Theorems

    Function: function-namep

    (defun function-namep (x wrld)
      (declare (xargs :guard (plist-worldp wrld)))
      (let ((__function__ 'function-namep))
        (declare (ignorable __function__))
        (and (symbolp x)
             (function-symbolp x wrld))))

    Theorem: booleanp-of-function-namep

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