		Search-engine friendly clone of the ACL2 documentation.

Defchoose2

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
(defsoft sofun)

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))