Filtering...

top

books/misc/hidden-defpkg-checks/top

Included Books

must-fail sub1 pkg1
other
(in-package "ACL2")
include-book
(include-book "std/testing/must-fail" :dir :system)
include-book
(include-book "sub1")
other
(must-fail (if (eq (fast-cert-mode state) t)
    (mv t nil state)
    (include-book "sub2")))
include-book
(include-book "pkg1")
other
(must-fail (if (eq (fast-cert-mode state) t)
    (mv t nil state)
    (defthm contradiction
      nil
      :hints (("Goal" :use ((:instance a-not-in-acl2-pkg (x (intern$ "B" "MY-PKG"))) (:instance a-in-acl2-pkg (x (intern$ "B" "MY-PKG"))))))
      :rule-classes nil)))