Index of modules


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]