NB. I haven't tried doing this with local named module defining an auxiliary function cf. #2411 because the scoping of such modules means that I end up having to write:
inits : List A → List (List A)
inits {A = A} = ([] ∷_) ∘ tail
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 {A = A} = λ (xs : List A) → xs ∷ tail xs
module Tails where
tail : List A → List (List A)
tail [] = []
tail (_ ∷ xs) = xs ∷ tail xs
which isn't obviously more readable/intelligible because of the artificiality of introducing an explicit λ ... on the RHS?
UPDATED: have gone with (a cleaned-up version of) this style now!
MatthewDaggitt
commented
3 months ago
NB. I haven't tried doing this with local named module defining an auxiliary function cf. #2411 because the scoping of such modules means that I end up having to write:
which isn't obviously more readable/intelligible because of the artificiality of introducing an explicit
λ ...on the RHS?UPDATED: have gone with (a cleaned-up version of) this style now!