Generate a singleton fixtype.
Some languages have a unit type, which consists of a single value. This is useful, for example, when some code returns nothing (besides presumably having some side effects), or as a component of larger types (e.g. a disjoint union of a detailed error value for failure and of the unit type for success without further information).
This macro introduces a fixtype consisting of a single keyword value. Given that ACL2 is an untyped language, the ability to customize the exact value of a unit type provides more flexibility, e.g. to create flat sums involving unit types, which requires such unit types to be disjoint from the other summand types, which are unknown a priori.
(defunit type :value ... ; no default :pred ... ; default type-p :fix ... ; default type-fix :equiv ... ; default type-equiv :parents ... ; no default :short ... ; no default :long ... ; no default )
The name of the new fixtype.
A keyword to be used as the (only) value of the new fixtype.
This must be provided, there is no default.
The name of the recognizer, fixer, and equivalence for the new fixtype.
The parents, short string, and long string for the XDOC topic generated for the new fixtype.
If any of these is not supplied, it is omitted from the XDOC topic; there are no defaults.
The following are generated, inclusive of XDOC documentation:
See the implementation, which uses a readable backquote notation, for details.