dhall-1.24.0: dhall-lang/Prelude/List/concat

{-
Concatenate a `List` of `List`s into a single `List`

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
```
-}
let concat
    : ∀(a : Type) → List (List a) → List a
    =   λ(a : Type)
      → λ(xss : List (List a))
      → List/build
        a
        (   λ(list : Type)
          → λ(cons : a → list → list)
          → λ(nil : list)
          → List/fold
            (List a)
            xss
            list
            (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
            nil
        )

in  concat