[Agda] Fwd: Ring Solver (looking for feedback)

[Matthew Daggitt]

Hi Oisin,
 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!).
Best,
Matthew

On Sun, Jan 27, 2019 at 3:39 PM Donnacha Oisín Kidney <mail at doisinkidney.com>
wrote:

> https://oisdk.github.io/agda-ring-solver/README.html
>
> 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.
>
> 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 1 ≈ 1 is
> ~5 seconds, versus the standard library’s ~2).
>
> 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).
>
> Anyway, this is what the interface looks like:
>
>     lemma : ∀ x y → x + y * 1 + 3 ≈ 3 + 1 + y + x + - 1
>     lemma = solve Int.ring
>
> Oisín Kidney.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190130/1a84bd46/attachment.html>