Filtering...

uguard-tests

books/std/system/uguard-tests

Included Books

uguard assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "uguard")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (uguard 'atom (w state)) *t*)
other
(assert-equal (uguard 'car (w state))
  '(if (consp x)
    't
    (equal x 'nil)))
other
(must-succeed* (defun f (x) (declare (xargs :guard (natp x))) x)
  (assert-equal (uguard 'f (w state)) '(natp x)))
other
(assert-equal (uguard '(lambda (z y) (binary-+ y (cons z '2))) (w state))
  *t*)