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-formulaallows all keywords, but only pays attention to
:guard-debug, which has the same effect as in
verify-guards(see guard-debug). Apply
verify-guards-formulato 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
defthmevent for which you want the guard proof obligation.
See guard-obligation if you want to obtain guard proof obligations for use in a program.