Def-gl-rule
A slightly enhanced version of def-gl-thm
def-gl-rule is a drop-in replacement for def-gl-thm that
adds:
- Integration with xdoc. You can give :parents, :short, and
:long documentation right at the top level of the defrule.
Support for Local
Another option is to provide a non-nil value to the keyword argument
:local. This results in surrounding the rule with a local.
Disabledp
Another option is to provide a non-nil value to the keyword argument
:disabledp (note the 'p' at the end). This results in disabling the new
rule after its proof finishes.
Some examples:
(def-gl-rule baz --> (local
... (encapsulate ()
:local t) (defthm baz ...)))
(def-gl-rule baz --> (defthm baz ...)
... (in-theory (disable baz))
:disabledp t)Subtopics
- Find-and-remove-key
- Remove keyword key and associated value from list lst
