Zulip Chat Archive

Stream: general

Topic: euclidean domains PR


view this post on Zulip Scott Morrison (Apr 04 2018 at 23:11):

I think https://github.com/leanprover/mathlib/pull/78 is at this point waiting either to be merged or for further comments.

view this post on Zulip Scott Morrison (Apr 04 2018 at 23:12):

I hope eventually it can be merged, so I can tick off the last box for Louis' summer project.

view this post on Zulip Mario Carneiro (Apr 05 2018 at 04:24):

I merged Louis' PR. There are some minor things that I notice, but it's best to just let that stuff evolve inside mathlib, it's gone through the ringer already and it came out nicely


Last updated: May 12 2021 at 23:13 UTC