Zulip Chat Archive

Stream: maths

Topic: nat.cast_coe


view this post on Zulip Joe Hendrix (Apr 03 2019 at 18:27):

We've run into performance problems when nat.cast_coe is triggered when we'd prefer to not have implicit coercisions. I'd like to hide the nat.cast_coe instance from Lean to avoid this implicit conversion. Is there a way to hide instances? Alternatively, would the mathlib folks consider turning nat.cast_coe into an ordinary declaration, and requiring users explicitly enable it with something like local attribute [instance] nat.cast_coe?

view this post on Zulip Johan Commelin (Apr 03 2019 at 18:32):

I would call that explicit enabling.

view this post on Zulip Joe Hendrix (Apr 03 2019 at 18:52):

Sorry, yes edited request.

view this post on Zulip Keeley Hoek (Apr 09 2019 at 14:48):

You can do attribute [-instance] nat.cast_coe to turn it off in-scope

view this post on Zulip Johan Commelin (Apr 09 2019 at 14:50):

Brilliant! That is going to be useful

view this post on Zulip Joe Hendrix (Apr 09 2019 at 18:09):

I tried

instance nat.cast_coe : has_coe nat string := sorry
local attribute [-instance] nat.cast_coe

I get test.lean:2:0: error: cannot remove attribute [instance]. This is with lean3.4.2, commit 1229f9b2d7f0.

view this post on Zulip Yury G. Kudryashov (Oct 15 2020 at 14:59):

What do you think about making docs#nat.cast_coe require add_monoid+has_one (or even semiring?) instead of has_one+has_zero+has_add?

view this post on Zulip Floris van Doorn (Oct 15 2020 at 19:15):

I'm not necessarily against it, but what would we gain by doing that?

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 03:45):

E.g., we won't have a coercion from nat to fin n.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 03:45):

So we'll be able to add a coercion in the other direction.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 03:46):

And we'll be able to define it as n •ℕ 1


Last updated: May 11 2021 at 15:12 UTC