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, then
it is treated as the body of a defthm event for which you want the
guard proof obligation.See guard-obligation if you want to obtain guard proof obligations for use in a program.
