• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
        • Primitive-functions
        • Translated-terms
        • Values
        • Evaluation
        • Program-equivalence
        • Functions
          • Function
          • Function-lookup
          • Function-option
          • Lift-function
          • Lift-function-list
          • Function-set
        • Packages
        • Programs
        • Interpreter
        • Evaluation-states
      • 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

• Functions

Lift-function-list

Lift a list of functions (specified by symbol) from the current ACL2 environment to the meta level, obtaining a set of functions.

Signature

(lift-function-list fns wrld) → functions

Arguments

fns — Guard (symbol-listp fns).

wrld — Guard (plist-worldp wrld).

Returns

functions — Type (function-setp functions).

Definitions and Theorems

Function: lift-function-list

(defun lift-function-list (fns wrld)
  (declare (xargs :guard (and (symbol-listp fns)
                              (plist-worldp wrld))))
  (let ((__function__ 'lift-function-list))
    (declare (ignorable __function__))
    (cond ((endp fns) nil)
          (t (insert (lift-function (car fns) wrld)
                     (lift-function-list (cdr fns) wrld))))))

Theorem: function-setp-of-lift-function-list

(defthm function-setp-of-lift-function-list
  (b* ((functions (lift-function-list fns wrld)))
    (function-setp functions))
  :rule-classes :rewrite)