How to debug the search for instances?

Stream: new members

[Martin C. Martin]

In Lean 4, you can use the class and instance to register things, that can later be found implicitly. I have a case where I think something should be found, but it isn't being found. I can't figure out why. Are there any tools for debugging the search for such implicit things?

[Kyle Miller]

One tool is setting set_option trace.Meta.synthInstance true

[Martin C. Martin]

Bruh. In the end, just exiting VS Code and re-starting it fixed it. ;(