Included Books
assert-bang
assert-bang-stobj
assert-equal
assert-qmark
eval
must-be-redundant
must-be-table-key
must-eval-to
must-eval-to-t
must-fail
must-fail-local
must-fail-with-error
must-fail-with-hard-error
must-fail-with-soft-error
must-not-be-table-key
must-not-prove
must-prove
must-succeed
must-succeed-star
constructors
other
(in-package "ACL2")
include-book
(include-book "assert-bang")
include-book
(include-book "assert-bang-stobj")
include-book
(include-book "assert-equal")
include-book
(include-book "assert-qmark")
include-book
(include-book "eval")
include-book
(include-book "must-be-redundant")
include-book
(include-book "must-be-table-key")
include-book
(include-book "must-eval-to")
include-book
(include-book "must-eval-to-t")
include-book
(include-book "must-fail")
include-book
(include-book "must-fail-local")
include-book
(include-book "must-fail-with-error")
include-book
(include-book "must-fail-with-hard-error")
include-book
(include-book "must-fail-with-soft-error")
include-book
(include-book "must-not-be-table-key")
include-book
(include-book "must-not-prove")
include-book
(include-book "must-prove")
include-book
(include-book "must-succeed")
include-book
(include-book "must-succeed-star")
include-book
(include-book "xdoc/constructors" :dir :system)
other
(defxdoc std/testing :parents (std testing-utilities) :short "A library of testing utilities." :long (topstring (p "These are utilities for creating tests. This library does not contain actual tests (other than perhaps tests for the testing utilities themselves), which are normally next to the code that they test. Note that @(see community-book) @('system/tests/') contains actual tests, for the ACL2 system code.")))