A library for working with stobjs.

- Stobj-updater-independence
- Discussion of the accessor/updater independence or
*frame problem*, especially as it relates to the def-updater-independence-thm utility. - Def-1d-arr
- Defines a abstract-stobj that logically just appears to be a typed list but is implemented as an array.
- Defstobj-clone
- Create a new stobj that is
:congruent-to an existing (concrete or abstract) stobj, and can be given to functions that operate on the old stobj. - Def-2d-arr
- Defines a abstract-stobj for a two-dimensional array.
- Defabsstobj-events
- Alternative to defabsstobj that tries to prove the necessary correspondence and preservation theorems instead of making you prove them ahead of time.
- Bitarr
- Abstract stobj: logically this just represents a list of
|ACL2|::|BITP| s, but it is implemented as an array. - Natarr
- Abstract stobj: logically this just represents a list of
|ACL2|::|NATP| s, but it is implemented as an array.