VERIFY-GUARDS-FORMULA

view the guard proof obligation, without proving it 
Major Section:  OTHER

See verify-guards and see guard for a discussion of guards. This utility is provided for viewing a guard proof obligation, without doing a proof.

Example Forms:
(verify-guards-formula foo)
(verify-guards-formula foo :guard-debug t)
(verify-guards-formula foo :otf-flg dont-care :xyz whatever)
(verify-guards-formula (+ (foo x) (bar y)) :guard-debug t)
Verify-guards-formula allows all keywords, but only pays attention to :guard-debug, which has the same effect as in verify-guards (see guard-debug). Apply verify-guards-formula to a name just as you would use verify-guards, but when you only want to view the formula rather than creating an event. If the first argument is not a symbol

See guard-obligation if you want to obtain guard proof obligations for use in a program.