Filtering...

assert-qmark-tests

books/std/testing/assert-qmark-tests

Included Books

assert-qmark assert-equal must-fail
other
(in-package "ACL2")
include-book
(include-book "assert-qmark")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-fail" :dir :system)
other
(assert-equal (assert? t 444) 444)
other
(assert-equal (assert? t 444 'my-ctx "my msg") 444)
other
(assert-equal (assert? t 444 'my-ctx (msg "my ~@0" "msg"))
  444)
other
(assert-equal (let ((x 4) (y 3))
    (assert? (> x y) 444))
  444)
other
(must-fail (progn (value-triple (assert? nil 444))))
other
(must-fail (progn (value-triple (assert? nil 444 'my-ctx "my msg"))))
other
(must-fail (progn (value-triple (assert? nil 444 'my-ctx (msg "my ~@0" "msg")))))
other
(must-fail (progn (value-triple (let ((x 4) (y 3))
        (assert? (< x y) 444)))))