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

Define-sk2

Introduce a second-order function via a second-order version of std::define-sk.

General Form

(define-sk2 sofun ...) ; same as define-sk

Inputs

The inputs are identical to std::define-sk.

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

Generated Events

(define-sk sofun ...) ; input form with define-sk2 replaced by define-sk
(defsoft sofun)

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

Subtopics

Define-sk2-implementation
Implementation of define-sk2.