Post-define-hook
A way to extend define to carry out additional behaviors.
The define macro can be configured with ``hooks'' to
automatically generate and submit certain additional events. For instance, the
fty::fixequiv-hook extends define to automatically prove certain
congruence rules.
This is an advanced and somewhat experimental feature. To introduce a new
post-define hook, first define a function of the signature:
(my-hook-fn defguts user-args state) -> (mv er val state)
Here:
- the defguts argument is a structure which will have information from
the define itself, see the comments in std/util/define.lisp for
details
- the user-args are any arguments that can be passed to your hook
function at define time via the :hooks argument, or via the default
post-define hook mechanism.
- the return value is an ordinary ACL2 error triple, where the val
should be some additional events to submit.
Once your function is defined, you can register it as a post-define hook as
follows:
(add-post-define-hook :myhook my-hook-fn)
And subsequently it will be legal to use :hooks ((:myhook ...)) or
similar. Define can also be configured with default post-define hooks, see
add-default-post-define-hook in the std/util/define.lisp source code;
also see the std/util/tests/define.lisp file for some working
examples.
