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