[Agda] proof by AC-reduction

[Serge D. Mechveliani]

On Wed, Feb 20, 2013 at 07:50:05PM +0100, Dan Ros?n wrote:
> Incidentally, I wrote one for distributive lattices:
> 
> http://web.student.chalmers.se/~danr/DLSolver/DLSolver.Examples.html
> 
> It was inspired by NAD's monoid solver.
> 

Thank you. I have to look into this.

------
Sergei


> On Wed, Feb 20, 2013 at 5:48 PM, Nils Anders Danielsson <nad at chalmers.se>
> wrote:
> 
> > 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?
> >
> >    http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html
> >    http://www.cse.chalmers.se/~nad/listings/lib/README.Integer.html
> >

> []