A | |
AAC_coq |
Interface with Coq where we define some handlers for Coq's API,
and we import several definitions from Coq's standard library.
|
AAC_helper |
Debugging functions, that can be triggered on a per-file base.
|
AAC_matcher |
Standalone module containing the algorithm for matching modulo
associativity and associativity and commutativity
(AAC).
|
AAC_print |
Pretty printing functions we use for the aac_instances
tactic.
|
AAC_rewrite |
Definition of the tactics, and corresponding Coq grammar entries.
|
AAC_search_monad |
Search monad that allows to express non-deterministic algorithms
in a legible maner, or programs that solve combinatorial problems.
|
AAC_theory |
Bindings for Coq constants that are specific to the plugin;
reification and translation functions.
|
B | |
Bool [AAC_coq] | |
C | |
Classes [AAC_coq] |
Coq typeclasses
|
Comparison [AAC_coq] | |
D | |
Debug [AAC_helper] | |
E | |
Equivalence [AAC_coq] | |
L | |
Leibniz [AAC_coq] | |
List [AAC_coq] |
Coq lists
|
N | |
Nat [AAC_coq] |
Coq unary numbers (peano)
|
O | |
Option [AAC_coq] | |
P | |
Pair [AAC_coq] |
Coq pairs
|
Pos [AAC_coq] |
Coq positive numbers (pos)
|
R | |
Relation [AAC_coq] | |
Rewrite [AAC_coq] | |
S | |
Sigma [AAC_theory] |
Environments
|
Stubs [AAC_theory] |
We need to export some Coq stubs out of this module.
|
Subst [AAC_matcher] |
Substitutions (or environments)
|
Sym [AAC_theory] |
Dynamically typed morphisms
|
T | |
Terms [AAC_matcher] |
Representations of expressions
|
Trans [AAC_theory] |
Tranlations between Coq and OCaml
|
Transitive [AAC_coq] |