type class inference for has_scalar

Stream: new members

[Jan-David Salchow]

The type class mechanism doesn't seem be able to figure out that functions to a normed space can be multiplied by scalars. Does anybody know why?

import analysis.normed_space algebra.pi_instances

-- works
example {α E : Type*} [vector_space ℝ E] (c : ℝ) (f : α → E) : ∀ x : α, (c • f) x  = c • (f x) := by simp

-- works
example {α E : Type*} [normed_space ℝ E] (c : ℝ) (f : α → E) :
  ∀ x : α, (@has_scalar.smul _ _ (@pi.has_scalar _ _ _ _) c f) x  =  c • (f x) :=
by simp

-- doesn't work
example {α E : Type*} [normed_space ℝ E] (c : ℝ) (f : α → E) : ∀ x : α, (c • f) x  = c • (f x) := by simp

[Mario Carneiro]

what is c • f?

[Mario Carneiro]

oh I see it's the pi instance