additions to style-guide (#2270)

* added stub content on programming idioms

* added para on qualified import names

Author: jamesmckinna

doc/style-guide.md

@@ -121,15 +121,31 @@ automate most of this.
 
 * If it is important that certain names only come into scope later in
   the file then the module should still be imported at the top of the
-  file but it can be given a shorter name using the keyword `as` and then
-  opened later on in the file when needed, e.g.
+  file but it can be imported *qualified*, i.e. given a shorter name
+  using the keyword `as` and then opened later on in the file when needed,
+  e.g.
   ```agda
   import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
   ...
   ...
   open SetoidEquality S
   ```
 
+* Naming conventions for qualified `import`s: if importing a module under
+  a root of the form `Data.X` (e.g. the `Base` module for basic operations,
+  or `Properties` for lemmas about them etc.) then conventionally, the
+  qualified name(s) for the import(s) should (all) share as qualfied name
+  that of the name of the `X` datatype defined: i.e. `Data.Nat.Base`
+  should be imported as `ℕ`, `Data.List.Properties` as `List`,  etc.
+  In this spirit, the convention applies also to (the datatype defined by)
+  `Relation.Binary.PropositionalEquality.*` which should be imported qualified
+  with the name `≡`.
+  Other modules should be given a 'suitable' qualified name based on its 'long'
+  path-derived name (such as `SetoidEquality` in the example above); commonly
+  occcurring examples such as `Algebra.Structures` should be imported qualified
+  as `Structures` etc.
+  NB. Historical legacy means that these conventions have not always been observed!
+
 * When using only a few items (i.e. < 5) from a module, it is a good practice to
   enumerate the items that will be used by declaring the import statement
   with the directive `using`. This makes the dependencies clearer, e.g.
@@ -532,3 +548,22 @@ word within a compound word is capitalized except for the first word.
 
 * The names of patterns for reflected syntax are also *appended* with an
   additional backtick.
+
+#### Specific pragmatics/idiomatic patterns
+
+## Use of `with` notation
+
+Thinking on this has changed since the early days of the library, with
+a desire to avoid 'unnecessary' uses of `with`: see Issues
+[#1937](https://github.com/agda/agda-stdlib/issues/1937) and
+[#2123](https://github.com/agda/agda-stdlib/issues/2123).
+
+## Proving instances of `Decidable` for sets, predicates, relations, ...
+
+Issue [#803](https://github.com/agda/agda-stdlib/issues/803)
+articulates a programming pattern for writing proofs of decidability,
+used successfully in PR
+[#799](https://github.com/agda/agda-stdlib/pull/799) and made
+systematic for `Nary` relations in PR
+[#811](https://github.com/agda/agda-stdlib/pull/811)
+