Define a set of mutually-recursive data types.
(defsums (my-term (my-atom val) (my-application (symbolp function) (my-term-list-p args))) (my-term-list (my-nil) (my-cons (my-term-p car) (my-term-list-p cdr))))
See defsum. This form is used when you want to define two or more
types which may be constructed from each other. In the above example,
Defsums accepts the same keyword arguments as defsum.
If you want some function to be defined inside the same mutual-recursion in which the recognizers for each of the sums and products are defined, you may insert the defun inside the def-mutual-sums form, i.e.
(defsums (foo (bla (bar-p x)) (ble (foo-p x) (bar-p y))) (bar (blu (integerp k)) (blo (symbolp f) (foo-list-p a))) (defun foo-list-p (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (foo-p (car x)) (foo-list-p (cdr x))))))
Usually it is not necessary to specify a measure for such a function; because there is currently no way of directly specifying the measures on the sums' recognizers, specifying an exotic measure on such a function is likely to fail.
As with defsum, def-mutual-sums requires the (possibly local) inclusion of the defsum-thms book.