Major Section: EVENTS
Example: (defequiv set-equal) is an abbreviation for (defthm set-equal-is-an-equivalence (and (booleanp (set-equal x y)) (set-equal x x) (implies (set-equal x y) (set-equal y x)) (implies (and (set-equal x y) (set-equal y z)) (set-equal x z))) :rule-classes (:equivalence))See equivalence.
General Form: (defequiv fn :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :event-name event-name :doc doc)where
fnis a function symbol of arity 2,
event-name, if supplied, is a symbol, and all other arguments are as specified in the documentation for
defequivmacro expands into a call of
defthm. The name of the
event-nameis supplied, in which case
event-nameis the name used. The term generated for the
defthmevent states that
fnis Boolean, reflexive, symmetric, and transitive. The rule-class
:equivalenceis added to the rule-classes specified, if it is not already there. All other arguments to the generated
defthmform are as specified by the other keyword arguments above.