From 4841532e90d321d6cf7f0769a193aa50cd24fee2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 7 Nov 2023 06:42:32 +0000 Subject: [PATCH 1/6] fix link to `installation-guide` --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index f9489e81f3..b4d513658a 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ 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 From 7e0c6a6b3691c22d7791ff77e5a1cdad36cdcc88 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Nov 2023 07:17:39 +0000 Subject: [PATCH 2/6] catching another reference to `notes/` --- doc/release-guide.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/release-guide.txt b/doc/release-guide.txt index 0296bc0fe1..0c60b5d4b3 100644 --- a/doc/release-guide.txt +++ b/doc/release-guide.txt @@ -3,7 +3,7 @@ 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` @@ -11,7 +11,7 @@ procedure should be followed: - `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. From 15e7080f7fa8f1f7f4d70098a13931bf97e9bcf9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Nov 2023 07:18:19 +0000 Subject: [PATCH 3/6] note on instance brackets --- doc/style-guide.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index a3c918e6a4..5732747cda 100644 --- a/doc/style-guide.md +++ b/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 From 7349ddb12049a38d966ea5f8d9f7613d8bc6e2db Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Nov 2023 07:20:04 +0000 Subject: [PATCH 4/6] `HACKING` guide --- HACKING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HACKING.md b/HACKING.md index b7573188b5..9b0e7454ac 100644 --- a/HACKING.md +++ b/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 From e29a425884070ad8b149f1fa5d59a2001aacc35c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 8 Nov 2023 07:55:33 +0000 Subject: [PATCH 5/6] added Gurmeet Singh's changes --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index b4d513658a..d1c83a3103 100644 --- a/README.md +++ b/README.md @@ -18,9 +18,9 @@ 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. From c2149f6999a9d564fd6536c364061243bae4af60 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Tue, 14 Nov 2023 10:10:08 +0000 Subject: [PATCH 6/6] [ fix ] links in README.md --- README.md | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index f9489e81f3..54967ebba9 100644 --- a/README.md +++ b/README.md @@ -18,20 +18,16 @@ 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.