diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 55 |
1 files changed, 55 insertions, 0 deletions
@@ -0,0 +1,55 @@ + + aac_tactics + =========== + + Thomas Braibant & Damien Pous + +Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France + + +FOREWORD +======== + +This plugin provides tactics for rewriting universally quantified +equations, modulo associativity and commutativity of some operators. + +INSTALLATION +============ + +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-aac-tactics + +DOCUMENTATION +============= + +Please refer to Tutorial.v for a succinct introduction on how to use +this plugin. + +To understand the inner-working of the tactic, please refer to the +.mli files as the main source of information on each .ml +file. Alternatively, [make world] generates ocamldoc/coqdoc +documentation in directories doc/ and html/, respectively. + +File Instances.v defines several instances for frequent use-cases of +this plugin, that should allow you to use it out-of-the-shelf. Namely, +we have instances for: + +- Peano naturals (Import Instances.Peano) +- Z binary numbers (Import Instances.Z) +- N binary numbers (Import Instances.N) +- P binary numbers (Import Instances.P) +- Rationnal numbers (Import Instances.Q) +- Prop (Import Instances.Prop_ops) +- Booleans (Import Instances.Bool) +- Relations (Import Instances.Relations) +- All of the above (Import Instances.All) + + +ACKNOWLEDGEMENTS +================ + +We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi +and Matthieu Sozeau for highly instructive discussions. + +This plugin took inspiration from the plugin tutorial "constructors", +distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau |