Rename things per review comments

agda · Mar 12, 2024 · 001bc7a · 001bc7a
1 parent 65b766b
commit 001bc7a
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 20 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -142,14 +142,14 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
-  applyUpTo-∷ʳ            : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
-  applyDownFrom-∷ʳ        : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
-  upTo-∷ʳ                 : upTo n ∷ʳ n ≡ upTo (suc n)
-  downFrom-∷ʳ             : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
-  applyUpTo-applyDownFrom : reverse (applyUpTo f n) ≡ applyDownFrom f n
-  upTo-downFrom           : reverse (upTo n) ≡ downFrom n
-  applyDownFrom-applyUpTo : reverse (applyDownFrom f n) ≡ applyUpTo f n
-  downFrom-upTo           : reverse (downFrom n) ≡ upTo n
+  applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
+  applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
+  upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
+  downFrom-∷ʳ           : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n)
+  reverse-applyUpTo     : reverse (applyUpTo f n) ≡ applyDownFrom f n
+  reverse-downFrom      : reverse (upTo n) ≡ downFrom n
+  reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n
+  reverse-downFrom      : reverse (downFrom n) ≡ upTo n
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
@@ -1190,27 +1190,27 @@ reverse-foldl f b xs = foldl-ʳ++ f b xs
 ------------------------------------------------------------------------
 -- reverse, applyUpTo, and applyDownFrom
 
-applyUpTo-applyDownFrom : ∀ (f : ℕ → A) n → reverse (applyUpTo f n) ≡ applyDownFrom f n
-applyUpTo-applyDownFrom f zero = refl
-applyUpTo-applyDownFrom f (suc n) = begin
+reverse-applyUpTo : ∀ (f : ℕ → A) n → reverse (applyUpTo f n) ≡ applyDownFrom f n
+reverse-applyUpTo f zero = refl
+reverse-applyUpTo f (suc n) = begin
   reverse (f 0 ∷ applyUpTo (f ∘ suc) n)  ≡⟨ reverse-++ [ f 0 ] (applyUpTo (f ∘ suc) n) ⟩
-  reverse (applyUpTo (f ∘ suc) n) ∷ʳ f 0 ≡⟨ cong (_∷ʳ f 0) (applyUpTo-applyDownFrom (f ∘ suc) n) ⟩
+  reverse (applyUpTo (f ∘ suc) n) ∷ʳ f 0 ≡⟨ cong (_∷ʳ f 0) (reverse-applyUpTo (f ∘ suc) n) ⟩
   applyDownFrom (f ∘ suc) n ∷ʳ f 0       ≡⟨ applyDownFrom-∷ʳ f n ⟩
   applyDownFrom f (suc n)                ∎
 
-upTo-downFrom : ∀ n → reverse (upTo n) ≡ downFrom n
-upTo-downFrom = applyUpTo-applyDownFrom id
+reverse-upTo : ∀ n → reverse (upTo n) ≡ downFrom n
+reverse-upTo = reverse-applyUpTo id
 
-applyDownFrom-applyUpTo : ∀ (f : ℕ → A) n → reverse (applyDownFrom f n) ≡ applyUpTo f n
-applyDownFrom-applyUpTo f zero = refl
-applyDownFrom-applyUpTo f (suc n) = begin
+reverse-applyDownFrom : ∀ (f : ℕ → A) n → reverse (applyDownFrom f n) ≡ applyUpTo f n
+reverse-applyDownFrom f zero = refl
+reverse-applyDownFrom f (suc n) = begin
   reverse (f n ∷ applyDownFrom f n)  ≡⟨ reverse-++ [ f n ] (applyDownFrom f n) ⟩
-  reverse (applyDownFrom f n) ∷ʳ f n ≡⟨ cong (_∷ʳ f n) (applyDownFrom-applyUpTo f n) ⟩
+  reverse (applyDownFrom f n) ∷ʳ f n ≡⟨ cong (_∷ʳ f n) (reverse-applyDownFrom f n) ⟩
   applyUpTo f n ∷ʳ f n               ≡⟨ applyUpTo-∷ʳ f n ⟩
   applyUpTo f (suc n)                ∎
 
-downFrom-upTo : ∀ n → reverse (downFrom n) ≡ upTo n
-downFrom-upTo = applyDownFrom-applyUpTo id
+reverse-downFrom : ∀ n → reverse (downFrom n) ≡ upTo n
+reverse-downFrom = reverse-applyDownFrom id
 
 ------------------------------------------------------------------------
 -- _∷ʳ_