Deffixequiv-sk-implementation
Implementation of deffixequiv-sk.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- wrld is the ACL2 world.
- fn and args are
the homonymous inputs of deffixequiv-sk.
- fn-witness is the witness function associated to fn.
See the option :skolem-name of defun-sk.
- fn-rule is the rewrite rule associated to fn.
See the option :thm-name of defun-sk.
- bvars are the bound (i.e. quantified) variables of fn.
- args-names is the list of argument names (without predicates)
from the args input.
- args-alist is an alist
from the names of the arguments
to their corresponding predicates.
In other words, it is args in alist form.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Deffixequiv-sk-lemma-insts-arg
- Generate lemma instances to prove the fixing of an argument.
- Deffixequiv-sk-lemma-insts-args
- Generate lemma instances to prove the fixing of all the arguments.
- Deffixequiv-sk-hints
- Generate the hints for deffixequiv.
- Deffixequiv-sk-lemma-inst-subst
- Generate instantiations for the bound variables.
- Deffixequiv-sk-fn
- Process the inputs and generate the deffixequiv.
- Deffixequiv-sk-macro-definition
- Definition of the deffixequiv-sk macro.
