nat.cast_coe

Stream: maths

[Joe Hendrix]

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?

[Johan Commelin]

I would call that explicit enabling.

[Joe Hendrix]

Sorry, yes edited request.

[Keeley Hoek]

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

[Johan Commelin]

Brilliant! That is going to be useful

[Joe Hendrix]

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.

[Yury G. Kudryashov]

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?

[Floris van Doorn]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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