Std/stobjs
A library for working with stobjs.
Subtopics
- 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.
