Zulip Chat Archive
Stream: lean4
Topic: Comment syntax highlighting
Jakob von Raumer (Dec 27 2025 at 10:29):
In VSCode, using < in a comment seems to break syntax highlighting:
/- i<T -/
example : Nat := 5
Marc Huisinga (Jan 12 2026 at 12:19):
This is vscode-lean4#656. We hope to resolve it by moving the markdown highlighting of the TextMate grammar to the semantic highlighting in the future.
Last updated: Feb 28 2026 at 14:05 UTC