You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is very much a work-in-progress and is not exhaustive.
4
+
This is very much a work-in-progress and is not exhaustive. Furthermore many of
5
+
these are aspirations, and may be violated in certain parts of the library.
6
+
It is hoped that at some point a linter will be developed for Agda which will
7
+
automate most of this.
5
8
6
9
## File structure
7
10
8
-
#### Module imports
9
-
10
-
* All module imports should be placed at the top of the file immediately
11
-
after the module declaration.
12
-
13
-
* If the module takes parameters that require imports from other files,
14
-
then those imports only may be placed above the module declaration.
15
-
16
-
* If it is important that certain names only come into scope later in
17
-
the file then the module should still be imported at the top of the
18
-
file but it can be given a shorter name using the keyword `as` and then
19
-
opened later on in the file when needed, e.g.
20
-
```agda
21
-
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
22
-
...
23
-
...
24
-
open SetoidEquality S
25
-
```
26
-
27
-
* Changing the naming of an imported item is performed with the [renaming](https://agda.readthedocs.io/en/latest/language/module-system.html#name-modifiers)
28
-
directive, e.g.
29
-
```agda
30
-
open import Agda.Builtin.Nat public
31
-
using (zero; suc) renaming (Nat to ℕ)
32
-
```
33
-
34
-
* The list of module imports should be declared in alphabetical order.
35
-
36
-
* When using only a few items from a module, it is a good practice to
37
-
enumerate the items that will be used by declaring the import statement
38
-
with the directive `using`. This makes the dependencies clearer, e.g.
39
-
```agda
40
-
open import Data.Nat.Properties public
41
-
using
42
-
( _≟_
43
-
; _≤?_ ; _≥?_ ; _<?_ ; _>?_
44
-
; _≤′?_; _≥′?_; _<′?_; _>′?_
45
-
; _≤″?_; _<″?_; _≥″?_; _>″?_
46
-
)
47
-
```
48
-
49
11
#### Indentation
50
12
51
13
* The contents of a top-level module should have zero indentation.
@@ -69,58 +31,100 @@ This is very much a work-in-progress and is not exhaustive.
69
31
should always go at the end of the line rather than the beginning of the
70
32
next line.
71
33
72
-
#### Module parameters
34
+
#### Modules
73
35
74
-
* Module parameters should be put on a single line if they fit.
75
-
76
-
* If they don't fit on a single line, then they should be spread out
77
-
over multiple lines, each indented by two spaces. If they can be
78
-
grouped logically by line then it is fine to do so, otherwise, a line
79
-
each is probably clearest.
36
+
* As a rule of thumb there should only be one named module per file. Anonymous
37
+
modules are fine, but named internal modules should either be opened publicly
38
+
immediately or split out into a separate file.
80
39
81
-
*The `where` keyword should be placed on an additional line of code at the end.
40
+
*Module parameters should be put on a single line if they fit.
82
41
83
-
* For example:
42
+
* Otherwise they should be spread out over multiple lines, each indented by two
43
+
spaces. If they can be grouped logically by line then it is fine to do so,
44
+
otherwise, a line each is probably clearest. The `where` keyword should be placed
45
+
on an additional line of code at the end. For example:
84
46
```agda
85
47
module Relation.Binary.Reasoning.Base.Single
86
48
{a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
87
49
(refl : Reflexive _∼_) (trans : Transitive _∼_)
88
50
where
89
51
```
52
+
53
+
* There should always be a single blank line after a module declaration.
90
54
91
-
#### Reasoning layout
55
+
#### Imports
92
56
93
-
* The `begin` clause should go on the same line as the rest of the proof.
57
+
* All imports should be placed in a list at the top of the file
58
+
immediately after the module declaration.
94
59
95
-
* Every subsequent combinator `_≡⟨_⟩_` should be placed on an additional
96
-
line of code, indented by two spaces.
60
+
* The list of imports should be declared in alphabetical order.
97
61
98
-
* The relation sign (e.g. `≡`) for each line should be aligned if possible.
62
+
* If the module takes parameters that require imports from other files,
63
+
then those imports only may be placed above the module declaration, e.g.
64
+
```agda
65
+
open import Algebra using (Ring)
66
+
67
+
module Algebra.Properties.Ring {a l} (ring : Ring a l) where
68
+
69
+
... other imports
70
+
```
99
71
100
-
* For example:
72
+
* If it is important that certain names only come into scope later in
73
+
the file then the module should still be imported at the top of the
74
+
file but it can be given a shorter name using the keyword `as` and then
75
+
opened later on in the file when needed, e.g.
101
76
```agda
102
-
+-comm : Commutative _+_
103
-
+-comm zero n = sym (+-identityʳ n)
104
-
+-comm (suc m) n = begin
105
-
suc m + n ≡⟨⟩
106
-
suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
107
-
suc (n + m) ≡⟨ sym (+-suc n m) ⟩
108
-
n + suc m ∎
77
+
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
78
+
...
79
+
...
80
+
open SetoidEquality S
109
81
```
110
82
111
-
* When multiple reasoning frameworks need to be used in the same file, the
112
-
`open` statement should always come in a where clause local to the
113
-
definition. This way users can easily see which reasoning toolkit is
114
-
being used. For instance:
83
+
* When using only a few items (i.e. < 5) from a module, it is a good practice to
84
+
enumerate the items that will be used by declaring the import statement
85
+
with the directive `using`. This makes the dependencies clearer, e.g.
115
86
```agda
116
-
foo m n p = begin
117
-
(...) ∎
118
-
where open ≤-Reasoning
87
+
open import Data.Nat.Properties using (+-assoc)
88
+
```
89
+
90
+
* Re-exporting terms from a module using the `public` modifier
91
+
should *not* be done in the list of imports as it is very hard to spot.
92
+
Instead the best approach is often to rename the import and then open it
93
+
publicly later in the file in a more obvious fashion, e.g.
94
+
```agda
95
+
-- Import list
96
+
...
97
+
import Data.Nat.Properties as NatProperties
98
+
...
99
+
100
+
-- Re-export ring
101
+
open NatProperties public
102
+
using (+-*-ring)
103
+
```
104
+
105
+
* If multiple import modifiers are used, then they should occur in the
106
+
following order: `public`, `using``renaming`, and if `public` is used
107
+
then the `using` and `renaming` modifiers should occur on a separate line.
108
+
For example:
109
+
```agda
110
+
open Monoid monoid public
111
+
using (ε) renaming (_∙_ to _+_)
119
112
```
120
113
121
-
#### Record layout
114
+
#### Layout of data declarations
115
+
116
+
* The `:` for each constructor should be aligned.
117
+
118
+
#### Layout of record declarations
122
119
123
-
* The `record` declaration should go on the same line as the rest of the proof.
120
+
* The `:` for each field should be aligned.
121
+
122
+
* If defining multiple records back to back then there should be a double
123
+
empty line between each record.
124
+
125
+
#### Layout of record instances
126
+
127
+
* The `record` keyword should go on the same line as the rest of the proof.
124
128
125
129
* The next line with the first record item should start with a single `{`.
126
130
@@ -129,6 +133,8 @@ line of code, indented by two spaces.
129
133
130
134
* The final line should end with `}` on its own.
131
135
136
+
* The `=` signs for each field should be aligned.
137
+
132
138
* For example:
133
139
```agda
134
140
≤-isPreorder : IsPreorder _≡_ _≤_
@@ -139,7 +145,7 @@ line of code, indented by two spaces.
139
145
}
140
146
```
141
147
142
-
#### `where` blocks
148
+
#### Layout of `where` blocks
143
149
144
150
*`where` blocks are preferred rather than the `let` construction.
145
151
@@ -153,8 +159,8 @@ line of code, indented by two spaces.
153
159
statement : Statement
154
160
statement = proof
155
161
where
156
-
proof : Proof
157
-
proof = some-very-long-proof
162
+
proof : Proof
163
+
proof = some-very-long-proof
158
164
```
159
165
160
166
* If the content of the block is trivial or is an `open` statement then
@@ -166,15 +172,89 @@ line of code, indented by two spaces.
166
172
where proof = x
167
173
```
168
174
169
-
#### Other
175
+
#### Layout of equational reasoning
176
+
177
+
* The `begin` clause should go on the same line as the rest of the proof.
178
+
179
+
* Every subsequent combinator `_≡⟨_⟩_` should be placed on an additional
180
+
line of code, indented by two spaces.
181
+
182
+
* The relation sign (e.g. `≡`) for each line should be aligned if possible.
183
+
184
+
* For example:
185
+
```agda
186
+
+-comm : Commutative _+_
187
+
+-comm zero n = sym (+-identityʳ n)
188
+
+-comm (suc m) n = begin
189
+
suc m + n ≡⟨⟩
190
+
suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
191
+
suc (n + m) ≡⟨ sym (+-suc n m) ⟩
192
+
n + suc m ∎
193
+
```
194
+
195
+
* When multiple reasoning frameworks need to be used in the same file, the
196
+
`open` statement should always come in a where clause local to the
197
+
definition. This way users can easily see which reasoning toolkit is
198
+
being used. For instance:
199
+
```agda
200
+
foo m n p = begin
201
+
(...) ∎
202
+
where open ≤-Reasoning
203
+
```
204
+
205
+
#### Mutual and private blocks
170
206
171
207
* Non-trivial proofs in `private` blocks are generally discouraged. If it is
172
208
non-trivial, then chances are that someone will want to reuse it at some
173
209
point!
174
210
211
+
* Instead private blocks should only be used to prevent temporary terms and
212
+
records that are defined for convenience from being exported by the module.
213
+
214
+
* The mutual block is considered obselete. Please use the standard approach
215
+
of placing the type signatures of the mutually recursive functions before
216
+
their definitions.
217
+
218
+
#### Function arguments
219
+
220
+
* Function arguments should be aligned between cases where possible, e.g.
221
+
```agda
222
+
+-comm : Commutative _+_
223
+
+-comm zero n = ...
224
+
+-comm (suc m) n = ...
225
+
```
226
+
227
+
* If an argument is unused in a case, it may at the author's
228
+
discretion be replaced by an underscore, e.g.
229
+
```agda
230
+
+-assoc : Associative _+_
231
+
+-assoc zero _ _ = refl
232
+
+-assoc (suc m) n o = cong suc (+-assoc m n o)
233
+
```
234
+
235
+
* If it is necessary to refer to an implicit argument in one case then
236
+
the implicit argument brackets must be included in every other case as
237
+
well, e.g.
238
+
```agda
239
+
m≤n⇒m∸n≡0 : ∀ {m n} → m ≤ n → m ∸ n ≡ 0
240
+
m≤n⇒m∸n≡0 {n = n} z≤n = 0∸n≡0 n
241
+
m≤n⇒m∸n≡0 {n = _} (s≤s m≤n) = m≤n⇒m∸n≡0 m≤n
242
+
```
243
+
244
+
* As of Agda 2.6.0 dot patterns are no longer necessary when unifying
245
+
function arguments and therefore should not be prepended to function
246
+
arguments.
247
+
248
+
#### Other
249
+
175
250
* The `with` syntax is preferred over the use of `case` from the `Function`
176
251
module.
177
252
253
+
* The standard library uses a standard line length of 72 characters. Please
254
+
try to stay within this limit. Having said that this is the most violated
255
+
rule in the style-guide and it is recognised that it is not always possible
256
+
to achieve whilst maintaining meaningful names.
257
+
178
258
## Types
179
259
180
260
#### Implicit and explicit arguments
@@ -187,10 +267,10 @@ line of code, indented by two spaces.
187
267
of proofs they should be extracted by using an anonymous module.
188
268
189
269
* Implicit of type `Level` and `Set` can be generalized using the keyword
190
-
`variable`. At the moment the policy is *not* to generalize over any other
191
-
types to minimize the amount of information that users have to keep in
192
-
their head concurrently.
193
-
270
+
`variable`. At the moment the policy is *not* to generalize over any other
271
+
types to minimize the amount of information that users have to keep in
272
+
their head concurrently.
273
+
194
274
## Naming conventions
195
275
196
276
* Names should be descriptive - i.e. given the name of a proof and the
@@ -208,24 +288,35 @@ word within a compound word is capitalized except for the first word.
208
288
209
289
#### Variables
210
290
291
+
* Sets are named `A`, `B`, `C` etc.
292
+
293
+
* Predicates are named `P`, `Q`, `R` etc.
294
+
295
+
* Relations are named either `R`, `S`, `T` in the general case
296
+
or `_≈_`/`_∼_`/`_≤_`/`_<_` if they are known to be an
0 commit comments