This macro introduces unary recognizers, and associated fixtypes, of true lists of values of fixtypes previously introduced via defbyte. This macro uses deflist to introduce the list fixtype, but it also generates various theorems, including some that relate the unary recognizers for lists of bytes to the aforementioned binary predicates for lists of bytes.
Besides their use in fixtypes,
the unary recognizers introduced by this macro support
(defbytelist type :elt-type :pred ... :fix ... :equiv ... :parents ... :short ... :long ... )
A symbol that specifies the name of the fixtype.
A symbol that names a fixtype previously introduced via defbyte. This is the fixtype of the elements of the generated list fixtype.
This input must be supplied; there is no default.
A symbol that specifies the name of the fixtype's recognizer. If this is
nil(the default), the name of the recognizer is typefollowed by -p.
A symbol that specifies the name of the fixtype's fixer. If this is
nil(the default), the name of the fixer is typefollowed by -fix.
A symbol that specifies the name of the fixtype's equivalence. If this is
nil(the default), the name of the equivalence is typefollowed by -equiv.
These, if present, are added to the XDOC topic generated for the fixtype.
A call of deflist to generate the fixtype.
Rule that rewrite between
predand the corresponding binary predicate ACL2::unsigned-byte-listp or ACL2::signed-byte-listp. These rules are disabled by default, but may be useful in some proofs. Since these are converse rules, a theory invariant is also generated preventing the enabling of both.
A rule to rewrite
fixapplied to take.
A rule to rewrite
fixapplied to rcons.
The above items are generated with XDOC documentation.