		Search-engine friendly clone of the ACL2 documentation.

Defun2

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

General Form

(defun2 sofun ...) ; same as defun

Inputs

The inputs are identical to defun.

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

Generated Events

(defun sofun ...) ; input form with defun2 replaced by defun
(defsoft sofun)

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

Examples

Example 1

;; A non-recursive function that applies four times
;; its function parameter to its individual parameter:
(defun2 quad[?f] (x)
  (?f (?f (?f (?f x)))))

Example 2

;; A recursive predicate that recognizes true lists
;; whose elements satisfy the predicate parameter:
(defun2 all[?p] (l)
  (cond ((atom l) (null l))
        (t (and (?p (car l)) (all[?p] (cdr l))))))

Example 3

;; A recursive function that homomorphically lifts ?F
;; to operate on true lists whose elements satisfy ?P:
(defun2 map[?f][?p] (l)
  (declare (xargs :guard (all[?p] l)))
  (cond ((endp l) nil)
        (t (cons (?f (car l)) (map[?f][?p] (cdr l))))))
;; The predicate parameter ?P only occurs in the guard, not in the body.

Example 4

;; A generic folding function on values as binary trees:
(defun2 fold[?f][?g] (bt)
  (cond ((atom bt) (?f bt))
        (t (?g (fold[?f][?g] (car bt)) (fold[?f][?g] (cdr bt))))))

Subtopics

Defun2-implementation: Implementation of defun2.