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