From 14fc21114003148c4111008d1dd0f8ba6b3d3091 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 19 Jun 2024 08:35:27 +0100
Subject: [PATCH] fixes #2411 (#2413)

* fixes #2411

* now via local -defined auxiliaries
---
 CHANGELOG.md                     |  4 ++--
 src/Data/List/Base.agda          | 20 ++++++++++----------
 src/Data/List/NonEmpty/Base.agda |  4 ++--
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9eb3d703eb..95de9d08dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -498,8 +498,8 @@ Additions to existing modules
 
 * In `Data.List.Base` redefine `inits` and `tails` in terms of:
   ```agda
-  tail∘inits : List A → List (List A)
-  tail∘tails : List A → List (List A)
+  Inits.tail : List A → List (List A)
+  Tails.tail : List A → List (List A)
   ```
 
 * In `Data.List.Membership.Propositional.Properties.Core`:
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index f707729af7..5c98372dc5 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -189,19 +189,19 @@ iterate : (A → A) → A → ℕ → List A
 iterate f e zero    = []
 iterate f e (suc n) = e ∷ iterate f (f e) n
 
-tail∘inits : List A → List (List A)
-tail∘inits []       = []
-tail∘inits (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail∘inits xs)
-
 inits : List A → List (List A)
-inits xs = [] ∷ tail∘inits xs
-
-tail∘tails : List A → List (List A)
-tail∘tails []       = []
-tail∘tails (_ ∷ xs) = xs ∷ tail∘tails xs
+inits {A = A} = λ xs → [] ∷ tail xs
+  module Inits where
+    tail : List A → List (List A)
+    tail []       = []
+    tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail xs)
 
 tails : List A → List (List A)
-tails xs = xs ∷ tail∘tails xs
+tails {A = A} = λ xs → xs ∷ tail xs
+  module Tails where
+    tail : List A → List (List A)
+    tail []       = []
+    tail (_ ∷ xs) = xs ∷ tail xs
 
 insertAt : (xs : List A) → Fin (suc (length xs)) → A → List A
 insertAt xs       zero    v = v ∷ xs
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index f332dcc162..35a3608a0f 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -146,12 +146,12 @@ ap fs as = concatMap (λ f → map f as) fs
 -- Inits
 
 inits : List A → List⁺ (List A)
-inits xs = [] ∷ List.tail∘inits xs
+inits xs = [] ∷ List.Inits.tail xs
 
 -- Tails
 
 tails : List A → List⁺ (List A)
-tails xs = xs ∷ List.tail∘tails xs
+tails xs = xs ∷ List.Tails.tail xs
 
 -- Reverse