Verify-guards-formula
View the guard proof obligation, without proving it
See verify-guards and see guard for a discussion of
guards. This utility, which does not evaluate its argument, provides output
showing the guard proof obligation (also known as the guard theorem) as
printed by verify-guards, but without then carrying out a proof attempt.
See also guard-formula-utilities for related utilities.
Example Forms:
(verify-guards-formula foo)
(verify-guards-formula foo :guard-debug t)
(verify-guards-formula foo :guard-debug t :guard-simplify :limited)
(verify-guards-formula foo :rrp t :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 and :guard-simplify, which have the same effect as in
verify-guards (also see guard-debug and guard-simplification), and to :rrp, described below. Apply
verify-guards-formula to a name just as you would use verify-guards, but when you only want the output that shows the guard proof
obligation, without attempting a proof or 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.
The :rrp argument (``return redundant p'') is nil by default. If
its value is not nil, then in the case that the first argument is a
guard-verified function symbol, the keyword :REDUNDANT is returned
without any output.
