search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Document `variable` block indentation style #2390

Closed JacquesCarette closed 1 month ago

JacquesCarette commented 1 month ago

As uncovered by PR #2389 it seems that the preferred style

private
  variable
    a : Level

isn't actually documented.

gallais commented 1 month ago

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.

JacquesCarette commented 1 month ago

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!

jamesmckinna commented 1 month ago

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...

JacquesCarette commented 1 month ago

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?

jamesmckinna commented 1 month ago

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...