Set.add not resolving

Stream: new members

[Javier Lopez-Contreras]

Hello!

I got an error that I cornered into this very minimal code. Why is Set.add not being used to infer Add (Set M)?

Thanks!

import Mathlib

variable {R : Type*} [Semiring R]

variable {M : Type*} [AddCommMonoid M] [Module R M]

#synth Add M

#check Set.add (α := M)

set_option diagnostics true in
#synth Add (Set M)

[Yaël Dillies]

You don't have open scoped Pointwise

[Javier Lopez-Contreras]

That was quick :)

[Javier Lopez-Contreras]

Thanks Yaël <3

[Kevin Buzzard]

The clue is in the source code (jump to definition with Set.add).

/-- The pointwise multiplication of sets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}` in
locale `Pointwise`. -/
@[to_additive
      "The pointwise addition of sets `s + t` is defined as `{x + y | x ∈ s, y ∈ t}` in locale
      `Pointwise`."]
protected def mul : Mul (Set α) :=
  ⟨image2 (· * ·)⟩

scoped[Pointwise] attribute [instance] Set.mul Set.add

the last line means "don't make this a global instance, only make it an instance when open scoped Pointwise is typed"

[Edward van de Meent]

i don't think you need scoped for this though?

[Edward van de Meent]

as in, open Pointwise works fine too

[Yaël Dillies]

Yes but it's good practice to differentiate between scopes and namespaces

[Edward van de Meent]

could you elaborate? i'm not sure what you mean by that...

[Kevin Buzzard]

I think open Pointwise opens both the scope (i.e. notation) and the namespace. I am usually careful to only open the scope if I don't need the namespace but probably others don't worry so much about this.