diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 55 |
1 files changed, 0 insertions, 55 deletions
@@ -1,55 +0,0 @@ - - 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 |