Zulip Chat Archive

Stream: new members

Topic: How to debug the search for instances?

Martin C. Martin (Nov 16 2023 at 18:40):

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 (Nov 16 2023 at 19:12):

One tool is setting set_option trace.Meta.synthInstance true

Martin C. Martin (Nov 16 2023 at 19:49):

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

Last updated: Dec 20 2023 at 11:08 UTC