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