Skip to content

Commit bab1cce

Browse files
committed
recommendation from agda#2294
1 parent d2ca7e8 commit bab1cce

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

doc/style-guide.md

+8
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,14 @@ automate most of this.
146146
as `Structures` etc.
147147
NB. Historical legacy means that these conventions have not always been observed!
148148

149+
* Qualified `open import`s should, in general, avoid `renaming`
150+
identifiers, in favour of using the long(er) qualified name,
151+
although similar remarks about legacy failure to observe this
152+
recommendation apply!
153+
NB `renaming` directives are, of course permitted when a module is
154+
imported qualified, in order to be *subsequently* `open`ed for
155+
`public` export (see below).
156+
149157
* When using only a few items (i.e. < 5) from a module, it is a good practice to
150158
enumerate the items that will be used by declaring the import statement
151159
with the directive `using`. This makes the dependencies clearer, e.g.

0 commit comments

Comments
 (0)