Zulip Chat Archive

Stream: new members

Topic: looking up instance definitions


view this post on Zulip Justus Springer (Mar 17 2021 at 09:31):

In this example:

import order.filter.basic

variables {α : Type*}

open filter

example (S T : set α) : principal S  principal T  S  T :=
begin
  sorry,
end

I would like to look up the definition of for filters. However, when I Ctrl+Click on it in VScode, I get referred to the general definition in the class has_le at core.lean. Is there a quick way to look up instance specific definitions like this?

view this post on Zulip Johan Commelin (Mar 17 2021 at 09:36):

variables (α : Type*)
#check (by apply_instance : has_le (filter α)) -- apparently `has_le` comes from `preorder`
#check (by apply_instance : preorder (filter α)) -- see `partial_order`
#check (by apply_instance : partial_order (filter α)) -- found it: `filter.partial_order`
#check filter.partial_order -- `Ctrl`-click here

view this post on Zulip Johan Commelin (Mar 17 2021 at 09:36):

I agree that it would be cool if there were a tactic that took care of the intermediate step.

view this post on Zulip Justus Springer (Mar 17 2021 at 09:38):

thanks, that's a cool trick!

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:11):

I always use the infoview for this now:
infoview.png

view this post on Zulip Johan Commelin (Mar 17 2021 at 10:11):

ooh, right, that makes a lot of sense (-;

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:12):

You just trace back to where something is actually defined and then jump to definition for the last thing.


Last updated: May 13 2021 at 20:13 UTC