fixes #2411 (#2413)

* fixes #2411

* now via local -defined auxiliaries

Author: jamesmckinna

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`:

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

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