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