This is analogous to deflist, defalist, and defomap. Besides the fixtype itself, this macro also generates some theorems about the fixtype. Future versions of this macro may generate more theorems, as needed.
Aside from the recognizer, fixer, and equivalence for the fixtype, this macro does not generate any operations on the typed osets. Instead, the generic oset operations can be used on typed osets. This macro generates theorems about the use of these generic operations on typed osets.
Future versions of this macro may be modularized to provide
a ``sub-macro'' that generates only the recognizer and theorems about it,
without the fixtype (and without the fixer and equivalence),
similarly to std::deflist and std::defalist.
That sub-macro could be called
(defset type :elt-type ... :elementp-of-nil ... :pred ... :fix ... :equiv ... :measure ... :parents ... :short ... :long ... )
The name of the new fixtype.
The (existing) fixtype of the elements of the new set fixtype.
nilis in the element fixtype :elt-type. It must be t, nil, or :unknown(the default). When tor nil, slightly better theorems are generated.
The name of the recognizer, fixer, and equivalence for the new fixtype.
The defaults are
typefollowed by -p, -fix, and -equiv.
These are used to generate XDOC documentation for the topic
If any of these is not supplied, the corresponding component is omitted from the generated XDOC topic.
This macro currently does not perform a thorough validation of its inputs. Erroneous inputs may result in failures of the generated events. Errors should be easy to diagnose, also since this macro has a very simple and readable implementation. Future versions of this macro should perform more thorough input validation.
The following are generated, inclusive of XDOC documentation:
See the implementation, which uses a readable backquote notation, for details.