Filtering...

stobjs-in-plus-tests

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

Included Books

stobjs-in-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "stobjs-in-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-in+ 'cons (w state)) '(nil nil))
other
(assert-equal (stobjs-in+ 'fmt (w state))
  '(nil nil nil state nil))
other
(must-succeed* (defstobj s)
  (defun f
    (x s state)
    (declare (ignore x s state)
      (xargs :stobjs (s state)))
    nil)
  (assert-equal (stobjs-in+ 'f (w state)) '(nil s state)))