From 7698bc77cd7692e0f1a25e8e0c631cf65c0d1b06 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 27 Sep 2023 12:57:59 +0900 Subject: [PATCH] Add style-guide note about local suffix --- notes/style-guide.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/notes/style-guide.md b/notes/style-guide.md index 2f9fa18553..d6201abe88 100644 --- a/notes/style-guide.md +++ b/notes/style-guide.md @@ -461,6 +461,16 @@ word within a compound word is capitalized except for the first word. map⁻ : Pointwise R (map f as) (map g bs) → Pointwise (λ a b → R (f a) (g b)) as bs ``` +* When specifying a property over a container, there are usually two choices. Either + assume the property holds for generally (e.g. `map id xs ≡ xs`) or a assume that + it only holds for the elements within the container (e.g. `All (λ x → f x ≡ x) xs → map f xs ≡ xs`). + The naming convention is to add a `-local` suffix on to the name of the latter variety. + e.g. + ```agda + map-id : map id xs ≡ xs + map-id-local : All (λ x → f x ≡ x) xs → map f xs ≡ xs + ``` + #### Keywords * If the name of something clashes with a keyword in Agda, then convention