Coercion in WithBot ℕ

Stream: mathlib4

[Violeta Hernández]

WithBot ℕ has both a coercion ℕ → WithBot ℕ given by docs#WithBot.some, and a Nat.cast map ℕ → WithBot ℕ via docs#WithBot.addMonoidWithOne. Both pretty-print as ↑n, and neither is a simp-normal form of the other, leading to annoying simp/norm_cast failures.

Should we make one of them canonical? If so, which one?

[Yury G. Kudryashov]

For ENat, the canonical one is Nat.cast.

[Violeta Hernández]

Sure, that works for me.

[Yury G. Kudryashov]

Note: I rarely use this part of the library. My message was about a related datapoint, not about making a decision.

[Eric Wieser]

I don't think you can win here without ending up back at a lean3-style "there is only one coercion function" position

[Eric Wieser]

Otherwise you have to duplicate all the some lemmas for Nat.cast, or vice versa, to keep things confluent