JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

Incorrect behaviour of command + / hotkey #546

Closed s3midetnov closed 2 months ago

s3midetnov commented 2 months ago

for a code sample like \func f \n=>5 (when => is on another line without any spaces before it) if you use "command + /" hotkey to comment the second line (or both lines) it does not comment the second line, but just inserts -- before =>, producing incorrect Arend code (--=> is not a correct commented line).