• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
          • Soft-future-work
          • Soft-macros
          • Updates-to-workshop-material
          • Soft-implementation
            • Soft-implementation-core
              • Sothm-inst-facts
              • Ext-fun-subst-term/terms/function
              • Fun-subst-function
              • Sothm-inst-pairs
              • Funvars-of-term/terms
              • Funvars-of-plain-fn
              • Sothm-inst-proof
              • Fun-subst-term/terms
              • Get-sof-instance
              • Sof-instancesp
              • Put-sof-instance
              • Fun-substp
              • Sofun-kindp
              • Funvar-listp
              • *-listp
              • Funvars-of-quantifier-fn
              • No-trivial-pairsp
              • Funvars-of-choice-fn
              • Funvar-instp
              • Funvars-of-thm
              • Sofunp
              • Funvarp
                • Sof-instances
                • Sothmp
                • Quant-sofunp
                • Plain-sofunp
                • Funvar-inst-listp
                • Choice-sofunp
                • Sofun-funvars
                • Sofun-kind
                • Function-variables-table
                • Sof-instances-table
                • Second-order-functions-table
              • Gen-macro2-of-macro
              • Defun-inst-implementation
              • Defthm-inst-implementation
              • Defsoft-implementation
              • Defunvar-implementation
              • Defund-sk2-implementation
              • Defun-sk2-implementation
              • Define-sk2-implementation
              • Defchoose2-implementation
              • Defund2-implementation
              • Defun2-implementation
              • Define2-implementation
            • Soft-notions
          • C
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Soft-implementation-core

    Funvarp

    Recognize names of function variables.

    Signature
    (funvarp funvar wrld) → yes/no
    Arguments
    wrld — Guard (plist-worldp wrld).
    Returns
    yes/no — Type (booleanp yes/no).

    These are symbols that name declared function variables, i.e. that are in the table of function variables.

    Definitions and Theorems

    Function: funvarp

    (defun funvarp (funvar wrld)
      (declare (xargs :guard (plist-worldp wrld)))
      (let ((__function__ 'funvarp))
        (declare (ignorable __function__))
        (let ((table (table-alist 'function-variables wrld)
    ))
          (and (symbolp funvar)
               (not (null (assoc-eq funvar table)))))))

    Theorem: booleanp-of-funvarp

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