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