Assert*
Create a guard proof obligation that given test holds
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,
a guard proof obligation is created that test holds, when used in
a definition made in logic-mode.
For a related utility, see 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.
Macro: assert*
(defmacro assert* (test form)
(cons 'and
(cons (cons 'mbt* (cons test 'nil))
(cons form 'nil))))
