[Agda] proof by AC-reduction

Nils Anders Danielsson nad at chalmers.se
Wed Feb 20 17:48:58 CET 2013

On 2013-02-19 15:50, Serge D. Mechveliani wrote:
> Agda needs some  proof assistants  provided as additional libraries
> (some of them may be even in the Standard library).

Have you seen the ring solver that is part of the standard library?


This solver uses a technique called "proof by reflection", a technique
that can be used for other solvers as well. For instance, I have written
one for monoids:


I have also written one for equality proofs (intended to be used with



More information about the Agda mailing list