[Agda] proof by AC-reduction
danr at student.chalmers.se
Wed Feb 20 19:50:05 CET 2013
Incidentally, I wrote one for distributive lattices:
It was inspired by NAD's monoid solver.
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?
> 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
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda