Incidentally, I wrote one for distributive lattices: <br><br><a href="http://web.student.chalmers.se/~danr/DLSolver/DLSolver.Examples.html">http://web.student.chalmers.se/~danr/DLSolver/DLSolver.Examples.html</a><br><br>It was inspired by NAD's monoid solver.<br>
<br><div class="gmail_quote">On Wed, Feb 20, 2013 at 5:48 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se" target="_blank">nad@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 2013-02-19 15:50, Serge D. Mechveliani wrote:<br>
> Agda needs some proof assistants provided as additional libraries<br>
> (some of them may be even in the Standard library).<br>
<br>
</div>Have you seen the ring solver that is part of the standard library?<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html" target="_blank">http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html</a><br>
<a href="http://www.cse.chalmers.se/~nad/listings/lib/README.Integer.html" target="_blank">http://www.cse.chalmers.se/~nad/listings/lib/README.Integer.html</a><br>
<br>
This solver uses a technique called "proof by reflection", a technique<br>
that can be used for other solvers as well. For instance, I have written<br>
one for monoids:<br>
<br>
<a href="http://www.cse.chalmers.se/edu/year/2012/course/afp/lectures/lecture11/html/Proof-by-reflection.html" target="_blank">http://www.cse.chalmers.se/edu/year/2012/course/afp/lectures/lecture11/html/Proof-by-reflection.html</a><br>
<br>
I have also written one for equality proofs (intended to be used with<br>
--without-K):<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/listings/equality/Equality.Tactic.html" target="_blank">http://www.cse.chalmers.se/~nad/listings/equality/Equality.Tactic.html</a><br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
/NAD<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</div></div></blockquote></div><br>