packages feed

dhall-1.3.0: Prelude/Natural/enumerate

{-
Generate a list of numbers from `+0` up to but not including the specified
number

Examples:

```
./enumerate +10 = [+0, +1, +2, +3, +4, +5, +6, +7, +8, +9] : List Natural

./enumerate +0 = [] : List Natural
```
-}
let enumerate : Natural → List Natural
    =   λ(n : Natural)
    →   List/build
        Natural
        (   λ(list : Type)
        →   λ(cons : Natural → list → list)
        →   List/fold
            { index : Natural, value : {} }
            (   List/indexed
                {}
                (   List/build
                    {}
                    (   λ(list : Type)
                    →   λ(cons : {} → list → list)
                    →   Natural/fold
                        n
                        list
                        (cons {=})
                    )
                )
            )
            list
            (λ(x : { index : Natural, value : {} }) → cons x.index)
        )

in  enumerate