Filtering...

eval

books/std/testing/eval

Included Books

must-be-redundant 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-prove must-prove must-succeed must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "must-be-redundant")
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-prove")
include-book
(include-book "must-prove")
include-book
(include-book "must-succeed")
include-book
(include-book "must-succeed-star")
other
(defsection ensure-error
  :parents (must-fail-with-error)
  :short "Deprecated synonym of @(tsee must-fail-with-error)"
  (defmacro ensure-error
    (&rest args)
    `(must-fail-with-error ,@ARGS)))
other
(defsection ensure-soft-error
  :parents (must-fail-with-soft-error)
  :short "Deprecated synonym of @(tsee must-fail-with-soft-error)"
  (defmacro ensure-soft-error
    (&rest args)
    `(must-fail-with-soft-error ,@ARGS)))
other
(defsection ensure-hard-error
  :parents (must-fail-with-hard-error)
  :short "Deprecated synonym of @(tsee must-fail-with-hard-error)"
  (defmacro ensure-hard-error
    (&rest args)
    `(must-fail-with-hard-error ,@ARGS)))
other
(defsection thm?
  :parents (must-prove)
  :short "Deprecated synonym of @(tsee must-prove)."
  (defmacro thm? (&rest args) `(must-prove ,@ARGS)))
other
(defsection not-thm?
  :parents (must-not-prove)
  :short "Deprecated synonym of @(tsee must-not-prove)."
  (defmacro not-thm? (&rest args) `(must-not-prove ,@ARGS)))