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