Currently fixtypes can only be associated to unary predicates, but ACL2::unsigned-byte-listp and ACL2::signed-byte-listp are binary predicates.
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.
A forward chaining rule from
predto the corresponding binary predicate ACL2::unsigned-byte-listp or ACL2::signed-byte-listp.
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 prove true-listp from
pred. Since true-listp is relatively common, this rule is disabled by default for efficiency.
A rule to rewrite
fixapplied to take.
A rule to rewrite
fixapplied to rcons.
The above items are generated with XDOC documentation.