• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
      • Std/util
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • 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
      • Defthm-domain
      • Event-macros
      • Def-universal-equiv
      • Def-saved-obligs
      • With-supporters-after
      • Definec
      • Sig
      • Outer-local
      • Data-structures
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
          • B*
          • Defunc
          • Fty
          • Apt
          • Std/util
          • Defdata
          • Defrstobj
          • Seq
          • Match-tree
          • Defrstobj
          • With-supporters
          • Def-partial-measure
          • Template-subst
          • 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
          • Defthm-domain
          • Event-macros
          • Def-universal-equiv
          • Def-saved-obligs
          • With-supporters-after
          • Definec
          • Sig
          • Outer-local
          • Data-structures
        • Trans1
        • Defmacro-untouchable
        • Set-duplicate-keys-action
        • Add-macro-alias
        • Magic-macroexpand
        • Defmacroq
        • Trans!
        • Remove-macro-fn
        • Remove-macro-alias
        • Add-binop
        • Untrans-table
        • Trans*-
        • Remove-binop
        • Tcp
        • Tca
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • 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.