attribute [instance, priority 10] coe_fn_trans

Stream: mathlib4

[Kevin Buzzard]

I was looking at what the ported data.fun_like.basic looks like. In the Lean 3 file there is

-- This instance should have low priority, to ensure we follow the chain
-- `fun_like → has_coe_to_fun`
attribute [instance, priority 10] coe_fn_trans

This is

instance coe_fn_trans {a : Sort u₁} {b : Sort u₂} {c : b → Sort v} [has_coe_to_fun b c]
  [has_coe_t_aux a b] : has_coe_to_fun a (λ x, c (@has_coe_t_aux.coe a b _ x)) :=
⟨λ x, coe_fn (@has_coe_t_aux.coe a b _ x)⟩

from core Lean 3. I feel ill-equipped to deal things here, I have only the vaguest understanding of coercions in Lean 3 and no understanding of them in Lean 4. Is this supposed to be here in Lean 4? There is also

variables {F α β} [i : fun_like F α β]

include i

@[priority 100, -- Give this a priority between `coe_fn_trans` and the default priority
  nolint dangerous_instance] -- `α` and `β` are out_params, so this instance should not be dangerous
instance : has_coe_to_fun F (λ _, Π a : α, β a) := { coe := fun_like.coe }

[Kevin Buzzard]

Related: core Lean 3 had a special name for the coercion to function:

@[reducible] def coe_fn {a : Sort u} {b : a → Sort v} [has_coe_to_fun a b] :
  Π x : a, b x :=
has_coe_to_fun.coe

Does core Lean 4 or mathlib4 have or want such a thing?

[Mario Carneiro]

Generally speaking, I would just suggest you comment these kinds of things out and put a porting note. These elaboration details are likely to be out of date anyway and will need to be redone in the new context

[Mario Carneiro]

The answer to the last question is has_coe_to_fun -> CoeFun