ACL2-pc::fail
(macro)
cause a failure
Examples:
fail
(fail t)
General Form:
(fail &optional hard)
This is probably only of interest to writers of macro commands. The only
function of fail is to fail to ``succeed''.
The full story is that fail and (fail nil) simply return (mv
nil nil state), while (fail hard) returns (mv hard nil state) if
hard is not nil. Also see ACL2-pc::do-strict, ACL2-pc::do-all, and ACL2-pc::sequence.