Introduce a second-order function via a second-order version of defun.
(defun2 sofun ...) ; same as defun
The inputs are identical to defun.
;; A non-recursive function that applies four times ;; its function parameter to its individual parameter: (defun2 quad[?f] (x) (?f (?f (?f (?f x)))))
;; 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))))))
;; 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.
;; 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))))))