Lean.Internal.CoeM

Stream: mathlib4

[Anatole Dedecker]

I noticed than we have some lemmas mentionning docs#Lean.Internal.CoeM (see this section). The docstring of Lean.Internal.CoeM explicitly says that this should not be used directly by users, but it appears "naturally" as the coercion form Set X to Set Y given a coercion from X to Y. Do we want to keep this ? Should we add a better name ? Should we change the definition from ⋃ x ∈ S, {↑x} (coming from a do definition) to the more natural (↑) '' S ?

[Eric Wieser]

I assume changing it from

@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
    [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
  let a ← x
  pure (CoeT.coe a)

to

@[inline, coe_decl] def Lean.Internal.coeM {m : Type u → Type v} {α β : Type u}
    [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
  CoeT.coe <$> x

would be enough?

[Eric Wieser]

Anatole Dedecker said:

but it appears "naturally" as the coercion form Set X to Set Y given a coercion from X to Y.

Only when X and Y are in the same universe

[Anatole Dedecker]

Eric Wieser said:

Anatole Dedecker said:

but it appears "naturally" as the coercion form Set X to Set Y given a coercion from X to Y.

Only when X and Y are in the same universe

Oh right so if we want this coercion we probably want a separate definition anyways. So indeed I think it's better to make sure that we don't use Lean.Internal.CoeM. Do you know which instance makes it trigger as a coercion though?