A | |
| Aac_rewrite |
Definition of the tactics, and corresponding Coq grammar entries.
|
B | |
| Bool [Coq] | |
C | |
| Classes [Coq] |
Coq typeclasses
|
| Comparison [Coq] | |
| 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 | |
| Leibniz [Coq] | |
| 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
|
| Transitive [Coq] |