ASSERT$
cause a hard error if the given test is false
Major Section: ACL2-BUILT-INS
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.
