intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Enumerations are rendered incorrectly in doc. comments

Open sxhya opened this issue 4 months ago • 2 comments

In this example leading "-"'s are part of doc. comment syntax. image

The example can be found in arend-lib/master

sxhya avatar Oct 10 '24 17:10 sxhya