• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • 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-term
                • Funvars-of-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
          • Bv
          • Imp-language
          • C
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Number-theory
          • Cryptography
          • Lists-light
          • Builtins
          • Axe
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Funvars-of-term/terms

    Funvars-of-terms

    Signature
    (funvars-of-terms terms wrld) → funvars
    Arguments
    terms — Guard (pseudo-term-listp terms).
    wrld — Guard (plist-worldp wrld).
    Returns
    funvars — A funvar-listp.