ASSERT$.html -- ACL2 Version 5.0

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.