From bab1cceea92ca2723765a630fe1ba04bf506e8a0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 3 Mar 2024 11:12:47 +0000 Subject: [PATCH 1/3] recommendation from #2294 --- doc/style-guide.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index 0e3a54841a..f87755e177 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -146,6 +146,14 @@ automate most of this. as `Structures` etc. NB. Historical legacy means that these conventions have not always been observed! +* Qualified `open import`s should, in general, avoid `renaming` + identifiers, in favour of using the long(er) qualified name, + although similar remarks about legacy failure to observe this + recommendation apply! + NB `renaming` directives are, of course permitted when a module is + imported qualified, in order to be *subsequently* `open`ed for + `public` export (see below). + * 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. From f00d4bdc6cf6c33d0006edff66830099d8ffccbc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 3 Mar 2024 11:16:11 +0000 Subject: [PATCH 2/3] spellcheck --- doc/style-guide.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index f87755e177..e19d22ef2b 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -134,7 +134,7 @@ automate most of this. * 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 + qualified name(s) for the import(s) should (all) share as qualified 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) @@ -142,7 +142,7 @@ automate most of this. 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 + occurring examples such as `Algebra.Structures` should be imported qualified as `Structures` etc. NB. Historical legacy means that these conventions have not always been observed! @@ -150,7 +150,7 @@ automate most of this. identifiers, in favour of using the long(er) qualified name, although similar remarks about legacy failure to observe this recommendation apply! - NB `renaming` directives are, of course permitted when a module is + NB. `renaming` directives are, of course permitted when a module is imported qualified, in order to be *subsequently* `open`ed for `public` export (see below). From 3a567a724338459412d47304f947a04c4b8316fe Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 3 Mar 2024 11:19:47 +0000 Subject: [PATCH 3/3] comma --- doc/style-guide.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/style-guide.md b/doc/style-guide.md index e19d22ef2b..184d354c0e 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -150,7 +150,7 @@ automate most of this. identifiers, in favour of using the long(er) qualified name, although similar remarks about legacy failure to observe this recommendation apply! - NB. `renaming` directives are, of course permitted when a module is + NB. `renaming` directives are, of course, permitted when a module is imported qualified, in order to be *subsequently* `open`ed for `public` export (see below).