File tree 1 file changed +10
-0
lines changed
1 file changed +10
-0
lines changed Original file line number Diff line number Diff line change @@ -461,6 +461,16 @@ word within a compound word is capitalized except for the first word.
461
461
map⁻ : Pointwise R (map f as) (map g bs) → Pointwise (λ a b → R (f a) (g b)) as bs
462
462
```
463
463
464
+ * When specifying a property over a container, there are usually two choices. Either
465
+ assume the property holds for generally (e.g. ` map id xs ≡ xs ` ) or a assume that
466
+ it only holds for the elements within the container (e.g. ` All (λ x → f x ≡ x) xs → map f xs ≡ xs ` ).
467
+ The naming convention is to add a ` -local ` suffix on to the name of the latter variety.
468
+ e.g.
469
+ ``` agda
470
+ map-id : map id xs ≡ xs
471
+ map-id-local : All (λ x → f x ≡ x) xs → map f xs ≡ xs
472
+ ```
473
+
464
474
#### Keywords
465
475
466
476
* If the name of something clashes with a keyword in Agda, then convention
You can’t perform that action at this time.
0 commit comments