Introduce a second-order function
via a second-order version of defchoose.
(defchoose2 sofun ...) ; same as defchoose
The inputs are identical to defchoose.
The function sofun must satisfy
all the requirements for defsoft,
because defchoose2 generates (defsoft sofun) (see below).
(defchoose sofun ...) ; input form with defchoose2 replaced by defchoose
sofun is introduced as a first-order function using defchoose.
It is also recorded as a second-order function via defsoft.
;; A function constrained to return a fixed point of ?F, if any exists:
(defchoose2 fixpoint[?f] x ()
(equal (?f x) x))
- Implementation of defchoose2.