Introduce an enumeration type, like an enum in C.
&key mode ; current defun-mode by default
parents ; nil by default
short ; nil by default
long ; nil by default
(:monday :tuesday :wednesday :thursday :friday :saturday :sunday))
results in a new function, (day-p x), that recognizes :monday,
Usage and Options
I often use keyword symbols as the elements, but any objects (even conses)
can be used.
The optional :mode keyword can be set to :logic or :program
to introduce the recognizer in logic or program mode. The default is whatever
the current default defun-mode is for ACL2, i.e., if you are already in program
mode, it will default to program mode, etc.
The optional :parents, :short, and :long parameters are like
those in defxdoc.
If keyword :disable-fc is set, it causes the generated forward chaining
rule to be disabled, which can make the admission of the defenum form and
subsequent proofs much faster when the number of elements is large.
If keyword :member is set, then the body of the recognizer uses a
member-eq check rather than an or. This can speed up compilation
when the number of elements is large. It is probably necessary to have some
rules about member-equal available; loading the std/lists/sets should
The recognizer just tests its argument against the elements, in order.
Because of this, you might want to order your elements so that the most common
elements come first. For instance, day-p will be fastest on :monday
and slowest on :sunday.
The recognizer uses eq or eql checks where possible, so if
your enumeration includes a mix of, say, conses and atom like symbols, you may
wish to put the atoms first.
Checking the argument against each element is probably a perfectly good
strategy when the number of elements is small (perhaps fewer than 20) and when
the equality checks are relatively fast (e.g., symbols, characters, numbers).
It is probably is not a good strategy otherwise. If you want to use defenum
for something more complex, it might be best to modify it to adaptively use a
fast alist or other schemes, based on the elements it is given.