Copy path to clipboardExamples
concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] ≡ "0, 1, 2"
concatMapSep ", " Natural Natural/show ([] : List Natural) ≡ ""
Source
{-
Transform each value in a `List` to `Text` and then concatenate them with a
separator in between each value
-}
let Status = < Empty | NonEmpty : Text >
let concatMapSep
: ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text
= λ(separator : Text)
→ λ(a : Type)
→ λ(f : a → Text)
→ λ(elements : List a)
→ let status =
List/fold
a
elements
Status
( λ(x : a)
→ λ(status : Status)
→ merge
{ Empty = Status.NonEmpty (f x)
, NonEmpty =
λ(result : Text)
→ Status.NonEmpty (f x ++ separator ++ result)
}
status
)
Status.Empty
in merge { Empty = "", NonEmpty = λ(result : Text) → result } status
let example0 =
assert : concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] ≡ "0, 1, 2"
let example1 =
assert : concatMapSep ", " Natural Natural/show ([] : List Natural) ≡ ""
in concatMapSep