		Search-engine friendly clone of the ACL2 documentation.

Defbytelist

Introduce a fixtype of true lists of unsigned or signed bytes of a specified size.

Introduction

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 tau system reasoning.

General Form

(defbytelist type
             :elt-type
             :pred ...
             :fix ...
             :equiv ...
             :parents ...
             :short ...
             :long ...
  )

Inputs

type

A symbol that specifies the name of the fixtype.

:elt-type

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.

:pred

A symbol that specifies the name of the fixtype's recognizer. If this is nil (the default), the name of the recognizer is type followed by -p.

:fix

A symbol that specifies the name of the fixtype's fixer. If this is nil (the default), the name of the fixer is type followed by -fix.

:equiv

A symbol that specifies the name of the fixtype's equivalence. If this is nil (the default), the name of the equivalence is type followed by -equiv.

:parents
:short
:long

These, if present, are added to the XDOC topic generated for the fixtype.

Generated Events

type

A call of deflist to generate the fixtype.

pred-forward-binpred

A forward chaining rule from pred to the corresponding binary predicate ACL2::unsigned-byte-listp or ACL2::signed-byte-listp.

binpred-rewrite-pred
pred-rewrite-binpred

Rule that rewrite between pred and 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.

true-listp-when-pred

A rule to prove true-listp from pred. Since true-listp is relatively common, this rule is disabled by default for efficiency.

fix-of-take

A rule to rewrite fix applied to take.

fix-of-rcons

A rule to rewrite fix applied to rcons.

The above items are generated with XDOC documentation.

Subtopics

Defbytelist-standard-instances: Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.
Defbytelist-implementation: Implementation of defbytelist.