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