From 4da2da6c2a33455f9700dc9344eb674b829b71c0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Thu, 30 May 2024 13:45:04 +0100
Subject: [PATCH] fixes #2390 (#2392)

---
 doc/style-guide.md | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/doc/style-guide.md b/doc/style-guide.md
index 2562f76cfd..c4b9af1bf8 100644
--- a/doc/style-guide.md
+++ b/doc/style-guide.md
@@ -229,6 +229,34 @@ automate most of this.
     }
   ```
 
+#### Layout of initial `private` block
+
+* Since the introduction of generalizable `variable`s (see below),
+  this block provides a very useful way to 'fix'/standardise notation
+  for the rest of the module, as well as introducing local
+  instantiations of parameterised `module` definitions, again for the
+  sake of fixing notation via qualified names.
+
+* It should typically follow the `import` and `open` declarations, as
+  above, separated by one blankline, and be followed by *two* blank
+  lines ahead of the main module body.
+
+* The current preferred layout is to use successive indentation by two spaces, eg.
+  ```agda
+  private
+    variable
+      a : Level
+      A : Set a
+  ```
+  rather than to use the more permissive 'stacked' style, available
+  since [agda/agda#5319](https://github.com/agda/agda/pull/5319).
+
+* A possible exception to the above rule is when a *single* declaration
+  is made, such as eg.
+  ```agda
+  private open module M = ...
+  ```
+
 #### Layout of `where` blocks
 
 * `where` blocks are preferred rather than the `let` construction.