This demonstrates a known issue: The parser is not aware of strings, thus, a closing block comment delimiter inside a string is taken as a closing block comment delimiter. Without nested comments: ```agda and other garbage @#$% that appears now as Agda code!" -} ``` With nested comments: ```agda This should be still commented-out. -} ``` The reverse situation: ```agda test = "Never put comment opening {- inside a string!" postulate ThisShouldNotBeCommentedOut : Set -- -} This should be text, not code!! ``` SNAFU.