Assert$
Cause a hard error if the given test is false
General Form:
(assert$ test form)
where test returns a single value and form is arbitrary.
Semantically, this call of assert$ is equivalent to form. However,
it causes a hard error if the value of test is nil. That hard error
invokes the function illegal, which has a guard that is equal
to nil; so if you use assert$ in code for which you verify guards,
then a proof obligation will be that the occurrence of test is never
nil.
See also assert*. Both assert$ and assert* create
a guard proof obligation (when used in a definition made in logic-mode). However, assert$ checks the assertion at runtime, while
assert* does not.
Also see assert-event for an assertion-checking utility that is an
event.
Subtopics
- Assert?
- A variation of assert$ with customizable context and message.
