		Search-engine friendly clone of the ACL2 documentation.

Mutual-recursion

Defuns

An alternative to mutual-recursion

Example:
(DEFUNS
 (evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))

General Form:
(DEFUNS defuns-tuple1 ... defuns-tuplen)

is equivalent to

(MUTUAL-RECURSION
  (DEFUN . defuns-tuple1)
  ...
  (DEFUN . defuns-tuplen))

In fact, defuns is the more primitive of the two and mutual-recursion is just a macro that expands to a call of defuns after stripping off the defun at the car of each argument to mutual-recursion. We provide and use mutual-recursion rather than defuns because by leaving the defuns in place, mutual-recursion forms can be processed by the Emacs tags program. See mutual-recursion.