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