Introduce a second-order function
via a second-order version of ACL2::defund-sk.
(defund-sk2 sofun ...) ; same as defund-sk
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).
(defund-sk sofun ...) ; input form with defund-sk2 replaced by defund-sk
sofun is introduced as a first-order function
It is also recorded as a second-order function via defsoft.
- Implementation of defund-sk2.