Defund-sk2
Introduce a second-order function
via a second-order version of ACL2::defund-sk.
General Form
(defund-sk2 sofun ...) ; same as defund-sk
Inputs
The inputs are identical to ACL2::defund-sk.
The function sofun must satisfy
all the requirements for defsoft,
because defund-sk2 generates (defsoft sofun) (see below).
Generated Events
(defund-sk sofun ...) ; input form with defund-sk2 replaced by defund-sk
(defsoft sofun)
sofun is introduced as a first-order function
using ACL2::defund-sk.
It is also recorded as a second-order function via defsoft.
Subtopics
- Defund-sk2-implementation
- Implementation of defund-sk2.
