		Search-engine friendly clone of the ACL2 documentation.

Defun-sk2

Introduce a second-order function via a second-order version of defun-sk.

(defun-sk sofun ...) ; same as defun-sk

The inputs are identical to defun-sk.

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

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

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

;; A predicate that recognizes injective functions:
(defun-sk2 injective[?f] ()
 (forall (x y) (implies (equal (?f x) (?f y)) (equal x y))))