Defund-sk
Define a function with quantifier
and disable it and its associated rewrite rule.
This is exactly like a defun-sk, except for two differences:
- It also generates an event to disable the function definition.
Thus, this macro is consistent with built-in macros like
defund and defund-nx.
- It also supports a :thm-enable input, nil by default,
that is used to generate, when nil, an event to disable
the rewrite rule associated to the function.
This rewrite rule is the one
whose name is controlled by the :thm-name option;
thus, the :thm-enable option of defund-sk2
is named consistently.
No disabling event is generated if :thm-enable is t;
the rewrite rule is left enabled.
Subtopics
- Defund-sk-implementation
- Implementation of defund-sk.
