Zulip Chat Archive

Stream: new members

Topic: type class inference for has_scalar


view this post on Zulip Jan-David Salchow (Nov 05 2018 at 15:07):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 15:10):

what is c • f?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 15:10):

oh I see it's the pi instance


Last updated: May 14 2021 at 12:18 UTC