• 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
  • 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.