search

agda / agda-stdlib

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

`style-guide` rule for initial `private` block in modules #2392

Closed jamesmckinna closed 4 months ago

jamesmckinna commented 4 months ago

Fixes #2390.

NB. The aim of the PR is to document what we (mostly) currently do, rather than fix in stone what we want to be able to do... the text is always changeable, and adherence to the guidelines a matter of manual review/checking!

jamesmckinna commented 4 months ago

I agree with this style. But we should probably get various people's buy-in, i.e. this should have a higher threshold than usual.

Absolutely!