From 48ab459be0cee4ee2760ca56f9b6cd685446231e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Jun 2024 06:39:31 +0100
Subject: [PATCH 1/2] fixes #2411

---
 CHANGELOG.md                     |  4 ++--
 src/Data/List/Base.agda          | 16 ++++++++--------
 src/Data/List/NonEmpty/Base.agda |  4 ++--
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9eb3d703eb..81e4112da8 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)
+  initsTail : List A → List (List A)
+  tailsTail : 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..5aff94f660 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)
+initsTail : List A → List (List A)
+initsTail []       = []
+initsTail (x ∷ xs) = [ x ] ∷ map (x ∷_) (initsTail xs)
 
 inits : List A → List (List A)
-inits xs = [] ∷ tail∘inits xs
+inits xs = [] ∷ initsTail xs
 
-tail∘tails : List A → List (List A)
-tail∘tails []       = []
-tail∘tails (_ ∷ xs) = xs ∷ tail∘tails xs
+tailsTail : List A → List (List A)
+tailsTail []       = []
+tailsTail (_ ∷ xs) = xs ∷ tailsTail xs
 
 tails : List A → List (List A)
-tails xs = xs ∷ tail∘tails xs
+tails xs = xs ∷ tailsTail 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..7efddec8c7 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.initsTail xs
 
 -- Tails
 
 tails : List A → List⁺ (List A)
-tails xs = xs ∷ List.tail∘tails xs
+tails xs = xs ∷ List.tailsTail xs
 
 -- Reverse
 

From 664357c598b01df31c79cc7545317d2028b971d4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Jun 2024 07:17:12 +0100
Subject: [PATCH 2/2] 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 81e4112da8..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
-  initsTail : List A → List (List A)
-  tailsTail : 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 5aff94f660..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
 
-initsTail : List A → List (List A)
-initsTail []       = []
-initsTail (x ∷ xs) = [ x ] ∷ map (x ∷_) (initsTail xs)
-
 inits : List A → List (List A)
-inits xs = [] ∷ initsTail xs
-
-tailsTail : List A → List (List A)
-tailsTail []       = []
-tailsTail (_ ∷ xs) = xs ∷ tailsTail 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 ∷ tailsTail 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 7efddec8c7..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.initsTail xs
+inits xs = [] ∷ List.Inits.tail xs
 
 -- Tails
 
 tails : List A → List⁺ (List A)
-tails xs = xs ∷ List.tailsTail xs
+tails xs = xs ∷ List.Tails.tail xs
 
 -- Reverse