Double line comments?

Stream: general

[Mario Carneiro]

I just noticed some peculiar syntax highlighting in vscode:

--- comment
def foo : ℕ := 1
#check foo

Note the three dashes. Here not just the comment line but also def foo : ℕ := 1 appear commented out, but lean (and reasonable readers) do not agree, the def foo line is not commented out.

[Reid Barton]

I think --- is a single-line docstring comment

[Reid Barton]

not that this explains vscode's behavior

[Mario Carneiro]

--- comment
  all

  these
  lines
  are

gray
not gray

[Reid Barton]

hmm it doesn't actually seem to behave like one, though

[Reid Barton]

don't know where I got that idea then

[Kevin Lacker]

the highlighting of --- lines works fine in emacs lean-mode fwiw

[Mario Carneiro]

I assume it's something particular to vscode's syntax highlighter. Clearly zulip's highlighter is also fine

[Gabriel Ebner]

This is an unintended interaction between the markdown and lean highlighting.

--- This is a single-item bullet-point list.