Aac_rewrite |
aac_rewrite -- rewriting modulo A or AC
|
Coq |
Interface with Coq where we define some handlers for Coq's API,
and we import several definitions from Coq's standard library.
|
Helper |
Debugging functions, that can be triggered on a per-file base.
|
Matcher |
Standalone module containing the algorithm for matching modulo
associativity and associativity and commutativity
(AAC).
|
Pretty printing functions we use for the aac_instances
tactic.
| |
Search_monad |
Search monad that allows to express non-deterministic algorithms
in a legible maner, or programs that solve combinatorial problems.
|
Theory |
Bindings for Coq constants that are specific to the plugin;
reification and translation functions.
|