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