In VSCode this results in everything beginning with {- being colored green (like a multiline comment) all the way to the end of the file, presumably because there is no closing -}
However, ucm validates this as correct code with x: Nat and x.doc : Doc.
So multiline comments inside a doc block are it seems ignored by ucm, but the VS Code highlighter attempts to parse them.
Indeed, > x.doc prints out
Paragraph
[ Word "this",
Word "is",
Word "a",
Word "doc",
Word "block",
Special (SpecialForm.Link (Right (Term.Term (Any 'link)))),
Word "{-",
Word "foo" ]
So it does seem like {- is a nothingburger for ucm when inside a doc block.
Drop this in a file
In VSCode this results in everything beginning with
{-
being colored green (like a multiline comment) all the way to the end of the file, presumably because there is no closing-}
However, ucm validates this as correct code with
x: Nat
andx.doc : Doc
.So multiline comments inside a doc block are it seems ignored by ucm, but the VS Code highlighter attempts to parse them.
Indeed,
> x.doc
prints outSo it does seem like
{-
is a nothingburger for ucm when inside a doc block.