# 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`.