## Stream: new members

### Topic: Coding standards: line breaks

#### Patrick Stevens (May 17 2020 at 11:34):

The documentation at https://leanprover-community.github.io/contribute/style.html says nothing about inserting blank lines in proofs; but mathlib seems to strongly prefer no blank lines, even in long proofs. Is this a formal requirement? It makes life harder in any editor that's paragraph-aware; I notice it because I use { and } very heavily in anything with vim bindings, and they are essentially useless in mathlib.

#### Patrick Massot (May 17 2020 at 11:34):

I don't think it's forbidden, but indeed it's not used much

#### Reid Barton (May 17 2020 at 11:37):

Don't "paragraph-aware" editors then become "proof-aware"?

#### Reid Barton (May 17 2020 at 11:38):

I don't really understand the difficulty (also, vim for lean??)

#### Reid Barton (May 17 2020 at 11:38):

Oh, "vim bindings", okay.

#### Reid Barton (May 17 2020 at 11:39):

The question seems a bit https://xkcd.com/1172/

#### Patrick Stevens (May 17 2020 at 11:45):

Sure, I'm not trying to warp the coding conventions just to make Vim work - if I were, I would mandate that lemmas look like this, so that [[ and ]] would work:

lemma foo () : nat :=
begin
{
}
end


#### Reid Barton (May 17 2020 at 11:45):

I think I've tried to put newlines in the middle of long proofs before, and someone told me to delete them, but it was long ago.

#### Patrick Stevens (May 17 2020 at 11:45):

Yeah, that happened to me a couple of days ago

#### Patrick Stevens (May 17 2020 at 11:46):

I can get around it by dropping marks all over the place or by doing a rough count of the number of lines I want to move when I incant a motion, it's just a bit more annoying than it could be

#### Reid Barton (May 17 2020 at 11:46):

I think the root cause is maybe not the lack of newlines in long proofs :upside_down:

#### Patrick Stevens (May 17 2020 at 11:47):

Aside from anything else, I am inclined to argue that newlines help readability a lot

#### Patrick Stevens (May 17 2020 at 11:47):

But if the will of the senate is no newlines, then I'll just get rid of them all in a linting pass pre commit, it's hardly the end of the world

#### Reid Barton (May 17 2020 at 11:48):

If you want to break up a proof with a newline for readability, it's probably even better to put a comment on that line.

#### Reid Barton (May 17 2020 at 11:58):

Long proofs should usually be structured with { }, at least.

Last updated: May 13 2021 at 21:12 UTC