Skip to content

Commit 3cc0b3c

Browse files
committed
Andreas's suggestions
1 parent c7af1ef commit 3cc0b3c

File tree

3 files changed

+12
-12
lines changed

3 files changed

+12
-12
lines changed

CHANGELOG.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -374,8 +374,8 @@ Additions to existing modules
374374

375375
* In `Data.List.Base` redefine `inits` and `tails` in terms of:
376376
```agda
377-
inits-tail : List A → List (List A)
378-
tails-tail : List A → List (List A)
377+
tail∘inits : List A → List (List A)
378+
tail∘tails : List A → List (List A)
379379
```
380380

381381
* In `Data.List.Membership.Setoid.Properties`:

src/Data/List/Base.agda

+8-8
Original file line numberDiff line numberDiff line change
@@ -189,19 +189,19 @@ iterate : (A → A) → A → ℕ → List A
189189
iterate f e zero = []
190190
iterate f e (suc n) = e ∷ iterate f (f e) n
191191

192-
inits-tail : List A List (List A)
193-
inits-tail [] = []
194-
inits-tail (x ∷ xs) = [ x ] ∷ map (x ∷_) (inits-tail xs)
192+
tail∘inits : List A List (List A)
193+
tail∘inits [] = []
194+
tail∘inits (x ∷ xs) = [ x ] ∷ map (x ∷_) (tail∘inits xs)
195195

196196
inits : List A List (List A)
197-
inits xs = [] ∷ inits-tail xs
197+
inits xs = [] ∷ tail∘inits xs
198198

199-
tails-tail : List A List (List A)
200-
tails-tail [] = []
201-
tails-tail (_ ∷ xs) = xs ∷ tails-tail xs
199+
tail∘tails : List A List (List A)
200+
tail∘tails [] = []
201+
tail∘tails (_ ∷ xs) = xs ∷ tail∘tails xs
202202

203203
tails : List A List (List A)
204-
tails xs = xs ∷ tails-tail xs
204+
tails xs = xs ∷ tail∘tails xs
205205

206206
insertAt : (xs : List A) Fin (suc (length xs)) A List A
207207
insertAt xs zero v = v ∷ xs

src/Data/List/NonEmpty/Base.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -146,12 +146,12 @@ ap fs as = concatMap (λ f → map f as) fs
146146
-- Inits
147147

148148
inits : List A List⁺ (List A)
149-
inits xs = [] ∷ List.inits-tail xs
149+
inits xs = [] ∷ List.tail∘inits xs
150150

151151
-- Tails
152152

153153
tails : List A List⁺ (List A)
154-
tails xs = xs ∷ List.tails-tail xs
154+
tails xs = xs ∷ List.tail∘tails xs
155155

156156
-- Reverse
157157

0 commit comments

Comments
 (0)