# Array1

A book of lemmas that characterize 1-dimensional arrays.

Because many of the functions characterized by this book are
non-recursive, one should always disable the theory
ARRAY1-FUNCTIONS after including this book, or the lemmas will not be
applicable.

The lemmas exported by this book should completely characterize
1-dimensional arrays for most purposes. Given the lemmas exported by this
book, it should not be necessary to enable any of the 1-dimensional
array functions except under special circumstances.

This book defines a function reset-array1 that clears an array,
effectively resetting each element of the array to the default value. This
book also includes a macro, defarray1type, which defines recognizers and
supporting lemmas for 1-dimensional arrays whose elements are all of a fixed
type.

### Subtopics

- Defarray1type
- Characterize 1-dimensional arrays with a fixed element type.
- Array1-lemmas
- A theory of all enabled rules exported by the array1 book.
- Reset-array1
- Clear an 1-dimensional array.
- Array1-functions
- A theory of all functions specific to 1-dimensional arrays.
- Array1-disabled-lemmas
- A theory of all rules exported DISABLEd by the "array1" book.