• 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
            • Define2-implementation
          • 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
  • Second-order-functions

Define2

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

General Form

(define2 sofun ...) ; same as define

Inputs

The inputs are identical to define.

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

Generated Events

(define sofun ...) ; input form with define2 replaced by define
(defsoft sofun)

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

Subtopics

Define2-implementation
Implementation of define2.