2 newlines before/after sections?

Stream: mathlib4

[Kenny Lau]

I personally think the code is easier to read if I insert 2 newlines before/after sections like this:

section Foo

/-- Lorem ipsum. -/
def Foo : sorry := sorry

theorem foo_eq_3 : Foo = 3 := sorry

end Foo


section Bar

/-- Dolor sit amet. -/
def Bar : sorry := sorry

theorem bar_eq_37 : Bar = 37 := sorry

end Bar

Is this acceptable in mathlib?

[Etienne Marion]

I don’t think there is a strict policy, so yes.

[Kevin Buzzard]

Note that VS Code now keeps track of what section you're in (look at the top of the file) so this sort of thing is far less of an issue than it was in Lean 3