Filtering...

must-fail-tests

books/std/testing/must-fail-tests

Included Books

must-fail must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "must-fail")
include-book
(include-book "must-succeed-star")
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y))))
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y))))
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y))))
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y)))
  :with-output-off nil
  :check-expansion t)
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y)))
  :with-output-off (summary))
other
(must-succeed* (defun f (x) x)
  (must-fail (defun f (x) (cons x x)))
  (defun g (x y) (f (cons x y)))
  :check-expansion t)