<div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Hi Oisin,<br></div><div dir="ltr"><div> This looks like great work! I'll try it out over the next couple of weeks. As mentioned before, please do feel free to start trying to incorporate it into the standard library (though it looks large enough that maybe splitting it over a few PRs might be wise!).</div><div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jan 27, 2019 at 3:39 PM Donnacha Oisín Kidney <<a href="mailto:mail@doisinkidney.com" target="_blank">mail@doisinkidney.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><a href="https://oisdk.github.io/agda-ring-solver/README.html" target="_blank">https://oisdk.github.io/agda-ring-solver/README.html</a><div><br></div><div>Hi all! For the past few months I’ve been working on a new ring solver to replace the one in the standard library. It’s part of my undergrad final year project, but I’m hoping to also submit it to a conference or something over the next few weeks.</div><div><br></div><div>The focus is on ease-of-use, but it’s also faster than the old solver (on more complex equations—the base-level time to solve things like <font face="Menlo" size="1">1 ≈ 1</font> is ~5 seconds, versus the standard library’s ~2).</div><div><br></div><div>At the moment, I’m the only person who’s used it, so I’m interested in hearing about more use cases and how it fits in. Also, any insight on type-checking performance would be great: the vast majority of speed gains in the solver came from places I wasn’t expecting (carefully arranging things to prevent reduction and encourage syntactic equality, for instance).</div><div><br></div><div>Anyway, this is what the interface looks like:</div><div><br></div><div><div><font face="Menlo">    lemma : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1</font></div><div><font face="Menlo">    lemma = solve Int.ring</font></div></div><div><br></div><div>Oisín Kidney.</div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</div></div>