Making projection notation work without an argument

Stream: general

[Heather Macbeth]

Is there a way to make projection notation work in the following example? I'm using docs#bounded_continuous_function.to_Lp, which doesn't have an explicit argument of a bounded_continuous_function α ℝ. It is a linear map from bounded_continuous_function α ℝ to some other module, so it can be coerced to a function from bounded_continuous_function α ℝ to that other module, and after the coercion it does have the right kind of explicit argument.

import measure_theory.lp_space

open measure_theory

local attribute [instance] fact_one_le_two_ennreal

noncomputable theory

variables {α : Type*} [topological_space α] [measure_space α] [borel_space α]
variables (μ : measure α) [finite_measure μ]

-- works
example (f : bounded_continuous_function α ℝ) : Lp ℝ 2 μ := bounded_continuous_function.to_Lp ℝ 2 μ ℝ f

/- fails:
invalid field notation, function 'bounded_continuous_function.to_Lp' does not have explicit argument with type (bounded_continuous_function ...)
-/
example (f : bounded_continuous_function α ℝ) : Lp ℝ 2 μ := f.to_Lp ℝ 2 μ ℝ

[Eric Wieser]

I think dot notation can only see through coe_fn if the definition has no explicit arguments

[Eric Wieser]

Which obviously in this case isn't an option

[Eric Wieser]

But maybe there's no good reason for this and we could change lean?

[Heather Macbeth]

Well, vote in favour from me!