NatCast

Stream: mathlib4

[Jon Eugster]

Is it correct that whenever I encounter a instance : Coe ℕ R := sorry that this should be instance NatCast R := instead? Does it make a difference?

[Eric Wieser]

Are there any such instances?

[Jon Eugster]

There is for example this in Data.ENat.Basic:

@[coe] def ofNat (n : ℕ) : ℕ∞ := WithTop.some n

instance : Coe ℕ ℕ∞ := ⟨ofNat⟩

and my question is would it change anything if that would say instance : NatCast ℕ∞ := ⟨ofNat⟩

[Eric Wieser]

The instance should probably just be removed, along with ofNat

[Eric Wieser]

It's already implied via docs#enat.add_comm_monoid_with_one

[Yury G. Kudryashov]

It would be nice to have a lemma/example/test

lemma ENat.natCast_def (n : Nat) : (n : ENat) = WithTop.some n := rfl

to be sure that the NatCast instance doesn't come from some generic recursive definition.

[Jon Eugster]

Thx, Ill add both suggestions to !4#1892 tonight

[Eric Wieser]

I'm not sure that ENat.natCast_def is a good idea as a lemma, as it unfolds the type synonym

[Eric Wieser]

Having it as an example would probably be more appropriate

[Eric Wieser]

We do seem to be missing docs#with_top.nat_cast_def though, which would be a suitable lemma

[Eric Wieser]

Ah, it's called docs#with_top.coe_nat

[Kevin Buzzard]

Back in the old days before norm_cast it was always a total mystery to me whether the lemma you wanted would have coe or cast in its name.