### ACL2-PC::NEGATE

(macro)
` `

run the given instructions, and ``succeed'' if and only if they ``fail''
Major Section: PROOF-CHECKER-COMMANDS

Example:
(negate prove)

General form:
(negate &rest instruction-list)

Run the indicated instructions exactly in the sense of `do-all`

, and
``succeed'' if and only if they ``fail''.**Remark:** `Negate`

instructions will never produce hard ``failures''.