Search for typeclass instance

Stream: new members

[Enrico Borba]

How do I go to the definition of a typeclass within either VS Code or the Mathlib docs? For example, I'm looking at the source of Mathlib/Order/Filter/Basic.lean and I see:

def Tendsto (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :=
  l₁.map f ≤ l₂

How do I see what the ≤ is referring to? I think it's the LE typeclass, but I'm not sure. Perhaps it's getting the ordering from a blanket impl of some other typeclass, or some typeclass extending LE like PartialOrder.

I'm curious how people go about this procedure in general rather than getting an answer to the specific answer with respect to Filter.

[Luigi Massacci]

If you hover over the ≤ in the infoview it will show @LE.le (Filter α) Preorder.toLE l₁ l₂ : Prop (an in general the typeclass for your symbol)

[Luigi Massacci]

That case is annoying because it won't appear in the infoview, but you can do something like this

variable (α : Type*) (l₁ : Filter α ) (l₂ : Filter α)
#check l₁ ≤ l₂

and hover over it thanks to the #check

[Enrico Borba]

Yeah it's annoying that I have to write an expression in #check to get it to show in the infoview. Good catch that you can see it there though. And there it's clear exactly where it's from.

[Enrico Borba]

Even once I find that out though, it's still annoying to get to the actual PartialOrder instance of Filter.

[Enrico Borba]

Not sure how other people do it, but I would search for instPartialOrderFilter in the mathlib docs (hoping that is the right name, which in this case it is). Not sure how else to go to the source from the infoview.

[Yaël Dillies]

You can do #synth LE (Filter α)