How can I generate a list of [0,1,...,n] from n?

Stream: lean4

[Juneyoung Lee]

This is a very naive question: given a nat n, how can I generate a list [0,1,..,n]?

[Juneyoung Lee]

Maybe [0,1,...,n-1] will be better, but either is fine.

[Adam Topaz]

docs#List.range

[Kyle Miller]

As a moogle.ai test, I just fed your question directly into it and List.range came up second, which is neat (thanks AI!)

query link

[Eric Wieser]

@loogle Nat -> List Nat

[loogle]

:search: List.iota, List.iotaTR, and 26 more

[Juneyoung Lee]

Thanks all.