list of natural numbers

Stream: new members

[Vaibhav Karve]

How can I create in Lean the (infinite) list of natural numbers? [0, 1, 2, 3, ...]

Things I have tried: list.range only gives me finite lists

Why I want to do this: I am interested in the list of primes. So I plan on writing list.filter nat.prime list_of_nat
which is why I need a way to write list_of_nat

[Kevin Buzzard]

list is by definition finite lists, so before we can answer your question about how to make a certain infinite list, you have to tell us what an infinite list is.

[Yakov Pechersky]

Can't you just speak about \all n, list.filter nat.prime (list.range n)?

[Yakov Pechersky]

We do have "infinite lists", phrased as docs#stream

[Yakov Pechersky]

But anything you might prove about them, you'd be proving about \all n, list.filter nat.prime (list.range n) on the way.