		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Defsums

Define a set of mutually-recursive data types.

Example:

(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, my-term and my-term-list could not be defined using independent defsum forms; their recognizer functions need to be defined in a mutual recursion.

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.