structure with class attribute vs class

Stream: general

[Bernd Losert]

I'm trying to get the following to work:

import tactic
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter

variable a : Type*

structure convergence_space (a : Type*) :=
(conv : filter a -> a -> Prop)

attribute [class] convergence_space

open convergence_space

def lim [convergence_space a] (l : filter a) : set a := set_of (conv l)

but it fails with a type mismatch error. It seems that Lean is confused about conv. I can fix this code by writing class convergence_space. But that causes other problems in the real code that I would rather avoid by doing it this way.

[Floris van Doorn]

Look at the type of conv (#check @conv): you will see that the convergence_space argument is explicit, because you declared it as structure, not as class.

[Floris van Doorn]

You want to make a separate version of conv' that has it as an instance implicit argument. We also do that in some places in mathlib.

import tactic
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter

variable {a : Type*}

structure convergence_space (a : Type*) :=
(conv' : filter a -> a -> Prop)

attribute [class] convergence_space

def convergence_space.conv {a : Type*} [convergence_space a] : filter a → a → Prop :=
convergence_space.conv' ‹_›

open convergence_space

def lim [convergence_space a] (l : filter a) : set a := {x | conv l x}

[Floris van Doorn]

one other change I made: change the variable line to variable {a : Type*}. You marked it as explicit, and that is going to bite you later.

[Bernd Losert]

When I do #check @conv, I get error: invalid '@', function is overloaded, use fully qualified names (overloads: conv, convergence_space.conv)

[Floris van Doorn]

I see. You can do any of

#check @convergence_space.conv
#print conv
#print convergence_space.conv

(beware though that #print gives very long outputs for non-trivial proofs)

[Bernd Losert]

But why is Lean confused about conv? Doesn't open convergence_space make it available without qualifying it with convergence_space.

[Floris van Doorn]

The problem is that there is already something called conv in Lean, so it might be useful (though it is not necessary) to rename your field.

[Bernd Losert]

Oh you're right. I will rename it then to avoid this.

[Floris van Doorn]

If you give Lean context which conv you mean, Lean will figure it out (like in my example above). However, in the #check line we give no such context.
The error you got originally is not because of overloading, but because of an explicit argument you didn't provide.

[Bernd Losert]

I thought the class attribute would make the first argument implicit, but I guess that's not the case.

[Bernd Losert]

Thanks for clarifying.