[Agda] proof by AC-reduction
Serge D. Mechveliani
mechvel at botik.ru
Thu Feb 21 09:34:41 CET 2013
On Wed, Feb 20, 2013 at 07:50:05PM +0100, Dan Ros?n wrote:
> Incidentally, I wrote one for distributive lattices:
> It was inspired by NAD's monoid solver.
Thank you. I have to look into this.
> On Wed, Feb 20, 2013 at 5:48 PM, Nils Anders Danielsson <nad at chalmers.se>
> > 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
More information about the Agda