|
|
|---|
|
|
|
|---|
Abstract stobj: logically this just represents a list of
This is a simple abstract stobj array, introduced by ACL2::def-1d-arr.
Definition:
(defabsstobj svexarr :foundation svexarr$c :recognizer (svexarrp :exec svexarr$cp :logic svexarr$ap) :creator (create-svexarr :exec create-svexarr$c :logic create-svexarr$a) :corr-fn svexarr$corr :exports ((svexs-length :exec svexs$c-length :logic svexs$a-length) (get-svex :exec svexs$ci :logic svexs$ai) (set-svex :exec update-svexs$ci :logic update-svexs$ai) (resize-svexs :exec resize-svexs$c :logic resize-svexs$a)))