Filtering...

stobjs-out-plus-tests

books/std/system/stobjs-out-plus-tests

Included Books

stobjs-out-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "stobjs-out-plus")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (stobjs-out+ 'cons (w state)) '(nil))
other
(assert-equal (stobjs-out+ 'fmt (w state)) '(nil state))
other
(must-succeed* (defstobj s)
  (defun f (x s) (declare (xargs :stobjs s)) (mv s x))
  (assert-equal (stobjs-out+ 'f (w state)) '(s nil)))