leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: VSCode folding of `section`/`namespace`


Alex Mobius (Nov 01 2024 at 15:40):

I want to be able to fold section/namespace declarations without increasing indentation. Can't seem to find it in the anguage extension options. Can someone help me out with configuring it? Not overtly familiar with VSCode language support.


Last updated: Dec 20 2025 at 21:32 UTC

Theme Simple by wildflame © 2016 Powered by jekyll