Viewing instantiations

Stream: new members

[Paul Nelson]

Is there a way to see which instances apply to a given type? I saw the following suggested in one the books, but they didn't work for me, so maybe they're out of date:

#print classes
#print instances inhabited
set_option trace.class_instances true

[Alex J. Best]

Which books are you looking at, there are quite a lot of differences between lean 3 and lean 4 so I'd recommend you stick to those aimed at lean 4 only

[Alex J. Best]

I think the easiest way to see this is on the docs, eg docs#Nat, if you click the dropdown "Instances for" you can see a list of all instances for nat defined in Mathlib (+Std + core). This is less helpful if you're working on your own project which adds a lot of stuff, but you can always run doc-gen4 on your project and get similar output

[Kyle Miller]

https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Instances.html#Std.Tactic.Instances.instancesCmd is useful

[Kyle Miller]

#instances Inhabited _ shows all Inhabited instances for example

[Paul Nelson]

Alex J. Best said:

Which books are you looking at, there are quite a lot of differences between lean 3 and lean 4 so I'd recommend you stick to those aimed at lean 4 only

https://lean-lang.org/theorem_proving_in_lean/type_classes.html, section 10.5

[Paul Nelson]

Guess I’ll switch to https://lean-lang.org/theorem_proving_in_lean4/ :)