Defisar-implementation
Implementation of defisar.
The implementation functions have arguments and results
consistently named as follows
(unless otherwise stated, explicitly or implicitly,
in the functions):
- state is the ACL2 state.
- ctx is the context used for errors.
- name is the homonymous input to the event macro.
- formula is the homonymous input to the event macro.
- proof is the homonymous input to the event macro.
- disable is the homonymous input to the event macro.
- rule-classes is the homonymous input to the event macro.
- hyps is the list of hypotheses of formula.
- concl is the conclusion of formula
- facts is an alist from keyword that identify facts
to information about those facts.
- bindings is an alist from variable symbols to formulas,
corresponding to the :let bindings.
Implementation functions' arguments and results
that are not listed above
are described in, or clear from,
those functions' documentation.
Subtopics
- Keyword-fact-info-alistp
- Recognize alists from keywords to fact information.
- Defisar-assume
- Execute an :assume command.
- Defisar-derive
- Execute a :derive command.
- Defisar-commands
- Execute a sequence of commands.
- Fact-infop
- Recognize information about facts.
- Defisar-qed
- Execute the :qed command.
- Defisar-let
- Execute a :let command.
- Defisar-derive-thm-hyps
- Generate the hypotheses for the theorem generated for
a :derive command.
- Defisar-proof
- Execute a proof.
- Defisar-fn
- Generate and submit the defisar events.
- Fact-info-listp
- Recognize lists of information about facts.
- Fact-info-list->thm-name-list
- Lift fact-info->thm-name to lists.
- Defisar-formula-to-hyps+concl
- Decompose the input formula into hypotheses and conclusion.
- Defisar-macro-definition-synonym
- Synonym of defisar in the "ACL2" package.
- Defisar-macro-definition
- Definition of the defisar macro.
