This library implements generalised rewriting based on the Coq approach and the paper "A New Look at Generalized Rewriting in TypeTheory" by Matthieu Sozeau.
- Constraint generation
- generate the same constraints coq does
- compare algorithm and constraints of the coq and the paper version
- Proof search
- recreate eauto efficiently to handle multiple related goals
- support adding theorems dynamically
- support adding tactics dynamically
- solve real-world grw problems
- idris port