dhall-1.24.0: dhall-lang/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 ]

./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