On this page:
generate-report
check-expect
check-within
check-error
Version: 4.2

2.8 "testing"

(include-book "testing" :dir :teachpacks)

This teachpack provides a graphical interface for unit tests.

(generate-report)

Write this at the end of your file to display the test results.

(check-expect actual expected)

Tests (equal actual expected).

(check-within actual expected delta)

Tests (and (<= (- expected delta) actual) (<= actual (+ expected delta))).

(check-error expr)

Tests that expr triggers a guard violation.