other
(in-package "STD")
other
(include-book "maybe-defthm")
other
(include-book "std/testing/assert-bang" :dir :system)
other
(maybe-defthm-as-rewrite foo (equal (car (cons x y)) x))
other
(maybe-defthm-as-rewrite baz (equal (stringp 'nil) 'nil))
other
(assert! (is-theorem-p 'foo (w state)))
other
(assert! (let ((ens (ens state)))
(active-runep '(:rewrite foo))))
other
(assert! (let ((ens (ens state)))
(not (active-runep '(:rewrite bar)))))
other
(enable-if-theorem foo)
other
(assert! (let ((ens (ens state)))
(active-runep '(:rewrite foo))))
other
(disable-if-theorem foo)
other
(assert! (let ((ens (ens state)))
(not (active-runep '(:rewrite foo)))))
other
(enable-if-theorem foo)
other
(assert! (let ((ens (ens state)))
(active-runep '(:rewrite foo))))