Zulip Chat Archive

Stream: mathlib4

Topic: data.int.gcd


Riccardo Brasca (Dec 13 2022 at 17:01):

I am porting data.int.gcd, see #981.

The file uses docs#int.nat_mod. This doesn't exist in mathlib4, right?

I know that mod is going to change in Std, so I am not fixing everything at the moment.

Riccardo Brasca (Dec 13 2022 at 17:09):

Oh, I just realized that it depends on data.int.order.basic, that is very far from having been ported :(

Scott Morrison (Dec 13 2022 at 23:05):

data.int.order.basic is now basically ready, it just has one error, so feel free to depend on it

Kevin Buzzard (Dec 13 2022 at 23:10):

my version has 0 errors ;-) (but it avoids the question which is actually at stake there)

Kevin Buzzard (Dec 13 2022 at 23:10):

(deleted)

Scott Morrison (Dec 13 2022 at 23:26):

https://github.com/leanprover-community/mathlib4/pull/980 is almost ready to go, but mysteriously in Mathlib.Tactic.Ring.Basic I had to make Ex[Base|Prod|Sum].evalPos partial. I don't see what change caused this, but I don't see how it could be problematic so I'm not going to wait on this. Just noting in case @Mario Carneiro sees some reason to be concerned.

Mario Carneiro (Dec 13 2022 at 23:49):

Note that there are already some definitions in there which are partial for performance, see Ex[Base|Prod|Sum].{eq,cmp}

Mario Carneiro (Dec 13 2022 at 23:50):

what happens if it's not marked as partial?

Riccardo Brasca (Dec 14 2022 at 09:07):

I am not sure I will have time today, if anyone wants to contribute to the PR please go ahead.


Last updated: Dec 20 2023 at 11:08 UTC