List instance priorities

Stream: lean4

[Michael Stoll]

Is there a way to get a list of all instances for, say, SMul together with their priorities?

I can do

import Mathlib

set_option trace.Meta.synthInstance true
#synth SMul _ _

and (after two clicks in the infoview) I can see the list of instances (ordered by increasing priority), but it does not show what the priorities are.

[Thomas Murrills]

Does the solution here work for you?

[Kyle Miller]

Std has #instances SMul _ _

[Thomas Murrills]

#instances doesn’t show priorities, though, right? (The quick code at the linked message does)

[Kyle Miller]

It shows them if the priority isn't 1000

[Eric Wieser]

@Henrik Böving, could we get the same priority-showing behavior in doc-gen?

[Henrik Böving]

image.png

soon on a documentation server nearby

[Michael Stoll]

Kyle Miller said:

It shows them if the priority isn't 1000

It also shows the signatures, which is more than I bargained for. I like the #show_instances "quick hack", though!