Showing automatically obtained typeclass instances

Stream: general

[Seul Baek]

Is it possible to show which instance Lean is using when it successfully performs a typeclass inference?

For instance, I know from the fact that I can use neg_le_neg with integers that Lean has silently performed a typeclass inference and found an instance of type ordered_comm_group int. But I don't know exactly which instance Lean has found. Is there a way to display this information, similar to how I can jump to definitions using f12?

[Kenny Lau]

you can print the proof of your theorem

[Kenny Lau]

using #print

[Kenny Lau]

and you can set pp.implicit true (there may be a better option) to see the implicit arguments, including the proof of the typeclass inference

[Scott Morrison]

set_option trace.class_instances true

[Kenny Lau]

well that displays too much information

[Seul Baek]

Thanks!

[Mario Carneiro]

you can also test instance problems with

theorem T : ordered_comm_group int := by apply_instance
#print T

[Kenny Lau]

#check (by apply_instance : ordered_comm_group int)

[Kenny Lau]

do I win?

[Mario Carneiro]

clever