		Search-engine friendly clone of the ACL2 documentation.

Deflist-of-len

Introduce a fixtype of lists of a specified length.

Introduction

deflist introduces fixtypes of lists of arbitrary lengths. Given such a fixtype, the macro deflist-of-len introduces a fixtype of those lists that have a specified length, along with some theorems that relate the recognizers, fixers, and equivalences of the two fixtypes.

The lists may be true or dotted, depending on the :true-listp option used in deflist. The macro deflist-of-len preserves that option.

Future versions of this macro could support richer constraints on list length than equality with a certain value, e.g. introduce fixtypes of lists of lengths below a certain value.

General Form

(deflist-of-len type
                :list-type ...
                :length ...
                :pred ...
                :fix ...
                :equiv ...
                :parents ...
                :short ...
                :long ...
  )

Inputs

type

A symbol that specifies the name of the fixtype.

:list-type

A symbol that names a fixtype previously introduced via deflist. This is the fixtype of the lists of arbitrary lengths, which are a superset of the lists of the generated fixtype.
The recognizer, fixer, and equivalence of the list fixtype must be all guard-verified. Let list-pred, list-fix and list-equiv be their names.
This input must be supplied; there is no default.

:length

A non-negative integer that specifies the length of the lists.
This input must be supplied; there is no default.

:pred

A symbol that specifies the name of the recognizer for type. 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 fixer for type. 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 equivalence for type. 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

pred

The recognizer for the fixtype, guard-verified.

booleanp-of-pred

A rewrite rule saying that pred is boolean-valued.

list-pred-when-pred-rewrite
list-pred-when-pred-forward

A rewrite rule and a forward chaining rule saying that a value satisfies list-pred when it satisfies pred.

len-when-pred-tau

A tau system rule saying that if a value satisfies pred then its length is the one specified by :length.

fix

The fixer for the fixtype, guard-verified.
It fixes values outside of pred by applying first take with the number specified by :length and then list-fix to the result.

pred-of-fix

A rewrite rule saying that fix always returns a value that satisfies pred.

fix-when-pred

A rewrite rule saying that fix disappears when its argument satisfies pred.

type
equiv

The fixtype, via a call of deffixtype that also introduces the equivalence equiv.

The above items are generated with XDOC documentation.

Subtopics

Deflist-of-len-implementation: Implementation of deflist-of-len.