Stream: Coq users

Topic: Lexer behavior on comments

view this post on Zulip Patrick Nicodemus (Jan 14 2024 at 23:06):

The lexer for Coq fails when one has imbalanced strings in a comment, i.e.
(* "a"" *)
Is this intended behavior? It is not easy to identify such typos as my ide does not highlight problems like this inside comments. Why is the lexer sensitive to this behavior?

view this post on Zulip Paolo Giarrusso (Jan 15 2024 at 00:56):

This should ease commenting out code with strings like "*)", right? I remember some advantage like this being discussed in the past

Last updated: Jun 13 2024 at 19:02 UTC