Zulip Chat Archive
Stream: lean4
Topic: breadcrumb confusion
Kevin Buzzard (Nov 23 2022 at 14:42):
Am I misunderstanding something? Is the breadcrumb thing telling me Swap is a namespace, when it's actually a section?
Sebastian Ullrich (Nov 23 2022 at 14:52):
Unfortunately the language server protocol has no idea what a section is
Sebastian Ullrich (Nov 23 2022 at 14:52):
We could of course print it as <section> Swap
Last updated: Dec 20 2023 at 11:08 UTC