fixes #2411 (#2413)

* fixes #2411

* now via local -defined auxiliaries

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