ACL2-PC_colon__colon_ORELSE.html -- ACL2 Version 3.1

(macro) run the first instruction; if (and only if) it ``fails'', run the second

Major Section:  PROOF-CHECKER-COMMANDS

Example:
(orelse top (print "Couldn't move to the top"))

General form:
(orelse instr1 instr2)

Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.

This instruction ``succeeds'' if and only if either instr1 ``succeeds'', or else instr2 ``succeeds''. If it ``fails'', then the failure is soft.