jump to instance definition

Stream: general

[Bernd Losert]

Is there a way to jump to the definition of an instance? For example, when I click on the sup symbol in f ⊔ g, where f and g are filters, I would like it to take me to the instance of has_sup for filters instead of taking me to the definition of the sup symbol. The only workaround for this that I know is to go to the mathlib docs page, find the definition of has_sup and search for the instances there.

[Adam Topaz]

You can use

#check (by apply_instance : Π α : Type*, has_sup (filter α))

to get the name, and chase it as far down as you would like

[Adam Topaz]

Doing so leads to docs#filter.complete_lattice

[Bernd Losert]

I see. Hmm... this is not really an improvement.

[Adam Topaz]

Well, once you get the name, you can use #check the_name and right click on the_name to go to the definition.

[Adam Topaz]

Yeah, it's not completely automatic, but it's better than nothing.

[Yaël Dillies]

You can inspect everything in the infoview!

[Adam Topaz]

that too!

[Adam Topaz]

some of us hermits still use emacs occasionally :speechless:

[Yaël Dillies]

Just click on the instances recursively (until you have exhausted the mathematically boring forgetful instances)

[Bernd Losert]

True, the infoview is better. However, I can't seem to use it on typeclass methods.

[Johan Commelin]

Why not?

[Bernd Losert]

I don't know. I don't get anything when I put the cursor on a typeclass method in a typeclass.

[Adam Topaz]

Peek-2022-11-01-14-54.gif

[Bernd Losert]

Yes, that works. But now try making type class with a method that uses F ⊔ G and try to get the infoview to show you F ⊔ G.

[Adam Topaz]

I'm not sure what you mean.

[Adam Topaz]

If you just have variables (X : Type*) [has_sup X] then there is nothing more to say! The has_sup instance was just an assumption!

[Adam Topaz]

But I'm probably misunderstanding what you want

[Bernd Losert]

In my case, I have this class:

@[ext] class convergence_space (α : Type*) :=
(converges : filter α → α → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {f g}, f ≤ g → ∀ {x}, converges g x → converges f x)

I want to see f ≤ g in the infoview so that I can get to the instance. Alas, it does not appear.

[Adam Topaz]

Peek-2022-11-01-15-15.gif

[Adam Topaz]

I didn't even need to include the (α : Type*) [convergence_space α], as you can see

[Bernd Losert]

I think you're misunderstanding. I'm interested in seeing f ≤ g from the type class itself in the infoview, not in some example using it.

[Adam Topaz]

what do you mean "from the typeclass itself"?

[Bernd Losert]

Well, you basically cheated by creating an example and then seeing the infoview for the example. Try getting the infoview without any example, i.e. just from looking at the code of the typeclass.

[Adam Topaz]

okay if you don't want to use the infoview, then you can do all that stuff with #check I mentioned above.

[Bernd Losert]

I want to use the infoview, but it's not available in that situation. It's the same thing in defs. It seems like the infoview only appears in tactic mode.

[Bernd Losert]

Thanks for helping though.

[Adam Topaz]

So put an

example : true :=
begin

end

above your definition as a temporary playground so you can use the infoview

[Bernd Losert]

Yes, I will add that to my scratch file where I normally use library_search and so on.

[Kyle Miller]

I wonder if it would ever be possible (in Lean 3 or Lean 4) to click on an expression and be able to inspect it with widgets. It'd be great to be able to more directly see how an expression is elaborated without these workarounds.

[Sebastian Ullrich]

It should be a pretty simple improvement of the "term goal view" to (optionally) show the term itself as well (edit: though that could be confusing in situations where the expected type differs from the inferred type). For the specific initial request, see also https://github.com/leanprover/lean4/pull/1767.