<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><a href="https://oisdk.github.io/agda-ring-solver/README.html" class="">https://oisdk.github.io/agda-ring-solver/README.html</a><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">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" class="">1 ≈ 1</font> is ~5 seconds, versus the standard library’s ~2).</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">Anyway, this is what the interface looks like:</div><div class=""><br class=""></div><div class=""><div class=""><font face="Menlo" class=""> lemma : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1</font></div><div class=""><font face="Menlo" class=""> lemma = solve Int.ring</font></div></div><div class=""><br class=""></div><div class="">Oisín Kidney.</div></body></html>