Document `variable` block indentation style about agda-stdlib HOT 5 CLOSED

The ability to stack layout keywords on a single line is only recent (agda/agda#5319)
so I would not say it's a preferred style, more of an accident of history.
I have no opinion on what the preferred style should be.

from agda-stdlib.

Indeed - well, this issue can still serve as a place to figure out what we want. As I prefer vertically-denser code, I'd be quite open to shifting to the stacked style!

from agda-stdlib.

Thanks for raising this @JacquesCarette and @omelkonian for drawing attention to it.

FWIW, I prefer the 'layered, indented' style, except when there is a single declaration, typically of a module declaration echoing an imported/parameter record in order to permit easier access to named/manifest fields equally.

Not least because not all opening private blocks contain only one kind of declaration...

PR incoming...

from agda-stdlib.

Certainly where there are multiple kinds of variable declarations, or a private block that has multiple things in it, we should go for the indented style.

I guess the main question is when it all naturally fits on one line and is conceptually a single thing, we should allow that?

from agda-stdlib.

I'm maybe (known to be) more profligate with whitespace, so perhaps not?

But the main criterion I guess should be consistency above all else...

from agda-stdlib.