dhall-1.3.0: Prelude/List/replicate

{-
Build a list by copying the given element the specified number of times

Examples:

```
./replicate +9 Integer 1 = [1, 1, 1, 1, 1, 1, 1, 1, 1] : List Integer

./replicate +0 Integer 1 = [] : List Integer
```
-}
let replicate : Natural → ∀(a : Type) → a → List a
    =   λ(n : Natural)
    →   λ(a : Type)
    →   λ(x : a)
    →   List/build
        a
        (   λ(list : Type)
        →   λ(cons : a → list → list)
        →   Natural/fold n list (cons x)
        )

in  replicate