Zulip Chat Archive

Stream: mathlib4

Topic: fixing library_note references


Thomas Murrills (Dec 14 2022 at 20:50):

Do library notes currently work? If so, how should references to them (e.g. note [reducible non-instances] be formatted in mathlib4?

Mario Carneiro (Dec 14 2022 at 20:51):

just like that

Thomas Murrills (Dec 14 2022 at 20:52):

Ok, neat. I noticed I couldn't command-click them like I can in mathlib, so I thought they might be formatted incorrectly.

Mario Carneiro (Dec 14 2022 at 20:53):

Not sure what we have to do to make that work (cc: @Gabriel Ebner ?)

Gabriel Ebner (Dec 14 2022 at 20:55):

Go-to-definition was implemented in the vscode extension without any help from the server. Maybe we can do something fancier directly in the server in the future, but for now we could also just copy the code from the Lean 3 vscode extension.


Last updated: Dec 20 2023 at 11:08 UTC