documentation: fix link to installation-guide, README.agda, README.md...

HACKING.md

@@ -4,7 +4,7 @@ Contributing to the library
 Thank you for your interest in contributing to the Agda standard library.
 Hopefully this guide should make it easy to do so! Feel free to ask any
 questions on the Agda mailing list. Before you start please read the
-[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
+[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md).
 
 What is an acceptable contribution?
 ===================================
@@ -124,7 +124,7 @@ git push USER -u new_feature
 
 You can then proceed to make your changes. Please follow existing
 conventions in the library, see
-[style-guide](https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md).
+[style-guide](https://github.com/agda/agda-stdlib/blob/master/doc/style-guide.md).
 for details. Document your changes in `agda-stdlib-fork/CHANGELOG.md`.
 
 If you are creating new modules, please make sure you are having a

README.md

@@ -18,23 +18,19 @@ If you're looking to find your way around the library, there are several
 different ways to get started:
 
 - The library's structure and the associated design choices are described
-in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/README.agda).
+in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/doc/README.agda).
 
-- The [README folder](https://github.com/agda/agda-stdlib/tree/master/README),
+- The [README folder](https://github.com/agda/agda-stdlib/tree/master/doc/README),
 which mirrors the structure of the main library, contains examples of how to
 use some of the more common modules. Feel free to [open a new issue](https://github.com/agda/agda-stdlib/issues/new) if there's a particular module you feel could do with
 some more documentation.
 
-- You can [browse the library's source code](https://agda.github.io/agda-stdlib/README.html)
+- You can [browse the library's source code](https://agda.github.io/agda-stdlib/)
 in glorious clickable HTML.
 
-- Finally, you can get an overview of the entire library by looking at the
-[index](https://agda.github.io/agda-stdlib/), which lists all modules
-in the library except the deprecated ones.
-
 ## Installation instructions
 
-See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md) for the latest version of the standard library.
+See the [installation instructions](https://github.com/agda/agda-stdlib/blob/master/doc/installation-guide.md) for the latest version of the standard library.
 
 #### Old versions of Agda
 

doc/release-guide.txt

@@ -3,15 +3,15 @@ procedure should be followed:
 
 #### Pre-release changes
 
-* Update `README.agda` by replacing 'development version' by 'version X.Y' in the title.
+* Update `doc/README.agda` by replacing 'development version' by 'version X.Y' in the title.
 
 * Update the version to `X.Y` in:
   - `agda-stdlib-utils.cabal`
   - `standard-library.agda-lib`
   - `CITATION.cff`
   - `CHANGELOG.md`
   - `README.md`
-  - `notes/installation-guide.txt`
+  - `doc/installation-guide.md`
 
 * Update the copyright year range in the LICENSE file, if necessary.
 

doc/style-guide.md

@@ -333,6 +333,16 @@ line of code, indented by two spaces.
   ...                  | false = filter p xs
   ```
 
+* Instance arguments, and their types, should use the vanilla ASCII/UTF-8 `{{_}}`
+  syntax in preference to the Unicode `⦃_⦄` syntax (written using `\{{`/`\}}`),
+  which moreover requires additional whitespace to parse correctly.
+  NB. Even for irrelevant instances, such as typically for `NonZero` arguments,
+  neverthelesss it is necessary to supply an underscore binding `{{_ : NonZero n}}`
+  if subsequent terms occurring in the type rely on that argument to be well-formed:
+  eg in `Data.Nat.DivMod`, in the use of `_/ n` and `_% n`
+  ```agda
+  m≡m%n+[m/n]*n : ∀ m n .{{_ : NonZero n}} → m ≡ m % n + (m / n) * n
+  ```
 
 ## Types