Safe-case
Error-checking alternative to case.
Safe-case is a drop-in replacement for case and is
logically identical to case. The only difference is that safe-case
adds some extra error-checking during execution.
In particular, when case is used and none of the cases match, the
answer is nil:
ACL2 !> (case 3
(1 'one)
(2 'two))
NIL
But when safe-case is used and none of the cases match, the result is
an error:
ACL2 !> (safe-case (+ 0 3)
(1 'one)
(2 'two))
HARD ACL2 ERROR in SAFE-CASE: No case matched:
(SAFE-CASE (+ 0 3) (1 'ONE) (2 'TWO)). Test was 3.
To use safe-case you need to include it, e.g.,:
(include-book "tools/safe-case" :dir :system)
