type class instance after ∀

Stream: new members

[Anders Kaseorg]

If I can do

[David Renshaw]

I don't know the answer to your question, but I was able to modify the second example to get it to typecheck:

def f : ∀ (α : Type) (h : has_add α) (x : α), @has_add.add α h x x = @has_add.add α h x x :=
λ (α : Type) (h : has_add α) (x : α), rfl

[David Renshaw]

and in Lean 4 this works:

def f : ∀ (α : Type) (h : Add α) (x: α), x + x = x + x :=
λ (α : Type) (h: Add α) (x : α) => rfl

[Eric Wieser]

by exactI is the solution here, searching for it will find other threads

[Kevin Buzzard]

But in short, has_add is a type class so you should be using square brackets and putting things before the colon so that the type class inference system can find them (note that the type class inference system does not look in the local context so that's why you get the error, however normally if a type class hypothesis has made it into the local context it's because square brackets were used)

[Eric Wieser]

Strictly the square brackets have nothing to do with it and have no effect inside the lemma they are arguments to, although typically you still want them for the users of you lemma