dhall-1.3.0: Prelude/List/concat

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

Examples:

```
./concat Integer
(   [   [0, 1, 2]    : List Integer
    ,   [3, 4]       : List Integer
    ,   [5, 6, 7, 8] : List Integer
    ]   : List (List Integer)
)
= [0, 1, 2, 3, 4, 5, 6, 7, 8] : List Integer

./concat Integer
(   [   [] : List Integer
    ,   [] : List Integer
    ,   [] : List Integer
    ]   : List (List Integer)
)
= [] : List Integer

./concat Integer ([] : List (List Integer)) = [] : List Integer
```
-}
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