(in-package "ACL2") (include-book "to-string") (defmacro check-expect (check expect) `(defthm ,(sexp->symbol `(check-expect ,check ,expect)) (equal ,check ,expect) :rule-classes nil)) (defmacro check-within (check expect within) `(defthm ,(sexp->symbol `(check-within ,check ,expect ,within)) (let ((check ,check) (expect ,expect) (within ,within)) (and (acl2-numberp check) (acl2-numberp expect) (acl2-numberp within) (>= check (- expect within)) (<= check (+ expect within)))) :rule-classes nil)) (defmacro check-error (check message) `(defthm ,(sexp->symbol `(check-error ,check ,message)) (or t ,check ,message) :rule-classes nil)) (defmacro generate-report () '(defconst *generate-report* t))