• 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
        • Set
        • Soft
          • Soft-future-work
          • Soft-macros
            • Defun-inst
            • Defequal
            • Defsoft
            • Defthm-inst
            • Defun2
            • Defunvar
              • Defunvar-implementation
            • Defun-sk2
            • Defchoose2
            • Defthm-2nd-order
            • Define-sk2
            • Defund-sk2
            • Define2
            • Defund2
          • Updates-to-workshop-material
          • Soft-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-macros
  • Function-variables

Defunvar

Introduce a function variable.

General Form

(defunvar fvar (* ... *) => *
  :print ...)

Inputs

fvar

A symbol, which names the function variable. It must be a valid function name that is not already in use.

(* ... *)

A list of zero or more * signs, which defines the arity of fvar.

:print ...

An option to customize the screen output: :all to print all the output; nil (the default) to print only any error output.

Generated Events

(defstub fvar (* ... *) => *)

fvar is introduced as an uninterpreted function with the given arity.

Examples

Example 1

;; A unary function variable:
(defunvar ?f (*) => *)

Example 2

;; A unary function variable:
(defunvar ?p (*) => *)

Example 3

;; A binary function variable:
(defunvar ?g (* *) => *)

Subtopics

Defunvar-implementation
Implementation of defunvar.