• 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
          • Defun-sk2
          • Defchoose2
          • Defthm-2nd-order
          • Define-sk2
          • Defund-sk2
          • Define2
          • Defund2
            • Defund2-implementation
        • 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
              • Defun-sk2
              • Defchoose2
              • Defthm-2nd-order
              • Define-sk2
              • Defund-sk2
              • Define2
              • Defund2
                • Defund2-implementation
            • 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
  • Second-order-functions

Defund2

Introduce a second-order function via a second-order version of defund.

General Form

(defund2 sofun ...) ; same as defund

Inputs

The inputs are identical to defund.

The function sofun must satisfy all the requirements for defsoft, because defund2 generates (defsoft sofun) (see below).

Generated Events

(defund sofun ...) ; input form with defund2 replaced by defund
(defsoft sofun)

sofun is introduced as a first-order function using defund. It is also recorded as a second-order function via defsoft.

Subtopics

Defund2-implementation
Implementation of defund2.