You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently Lean code is folded like C code, where everything is folded until the next token with less indentation (usually the closing curly brace), including empty lines. That will fold away any separating line breaks between two definitions, making it harder to read. I think the folding style of e. g. Python is better suited for Lean, since we don't have closing curly braces for every indentation level.
VSC has an option for the language-configuration.json file to change that, by adding the option "folding": { "offSide": true }, as mentioned in microsoft/vscode#3353 (comment).
The text was updated successfully, but these errors were encountered:
Currently Lean code is folded like C code, where everything is folded until the next token with less indentation (usually the closing curly brace), including empty lines. That will fold away any separating line breaks between two definitions, making it harder to read. I think the folding style of e. g. Python is better suited for Lean, since we don't have closing curly braces for every indentation level.
VSC has an option for the language-configuration.json file to change that, by adding the option
"folding": { "offSide": true }
, as mentioned in microsoft/vscode#3353 (comment).The text was updated successfully, but these errors were encountered: