ACL2-PC::FAIL

(macro) cause a failure 
Major Section:  PROOF-CHECKER-COMMANDS


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. See also do-strict, do-all, and sequence.