/Prelude-v16.0.0/List/concat

Copy path to clipboard

Examples

  concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ]
≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
  concat Natural [ [] : List Natural, [] : List Natural, [] : List Natural ]
≡ ([] : List Natural)
concat Natural ([] : List (List Natural)) ≡ ([] : List Natural)

Source

{-
Concatenate a `List` of `List`s into a single `List`
-}
let concat
: ∀(a : Type) → List (List a) → List a
= λ(a : Type)
→ λ(xss : List (List a))
→ List/build
a
( λ(list : Type)
→ λ(cons : alistlist)
→ λ(nil : list)
→ List/fold
(List a)
xss
list
(λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
nil
)

let example0 =
assert
: concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ]
≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]

let example1 =
assert
: concat
Natural
[ [] : List Natural, [] : List Natural, [] : List Natural ]
≡ ([] : List Natural)

let example2 =
assert : concat Natural ([] : List (List Natural)) ≡ ([] : List Natural)

in concat