comment block

Stream: general

[Paul van Wamelen]

What is the correct way to comment out a big block of code? If I use either '/-' or '/--' and a closing '-/' I often get strange errors further down the file. Often saying "unexpected end of comment block".

[Yakov Pechersky]

The safest way is -- at the start of every line

[Yakov Pechersky]

/-- ... -/ has special meaning re docstrings and those can't be associated with some declarations

[Kevin Buzzard]

/-
...
-/

should work fine. If you get weird errors then just restart Lean -- I agree that there is some comment block bug (adding them and removing them quickly can confuse Lean) but restarting Lean always fixes it immediately.