Cannot synthesize placeholder

Stream: new members

[Vasily Ilin]

Why does this not work? Getting an error at submodule.span k {v1, v2}.

import tactic
import linear_algebra.basis
import linear_algebra.finite_dimensional

open submodule

variables (k : Type) [field k] (V : Type) [add_comm_group V] [module k V]

variables (v1 : V) (v2 : V)

example : submodule.span k {v1, v2} = submodule.span k {v1, v2} :=
begin
  sorry,
end

[Eric Rodriguez]

you'll have to tag {v1, v2} with set V

[Kevin Buzzard]

example : submodule.span k ({v1, v2} : set V) = submodule.span k {v1, v2} :=
begin
  sorry,
end

works. The reason is that {v1,v2} notation can mean a lot of things; you need to tell the elaborator you're talking about a subset of V.

[Eric Rodriguez]

lean isn't very good at inferring {a, b, ...}'s type

[Vasily Ilin]

Thank you!