Included Books
other
(in-package "ACL2")
include-book
(include-book "assert-equal")
include-book
(include-book "must-fail")
include-book
(include-book "must-succeed-star")
other
(must-succeed* (defun f (x) (cons x x)) (assert-equal (f 3) '(3 . 3)))
other
(must-fail (assert-equal 1 2))