## Stream: new members

### Topic: list of natural numbers

#### Vaibhav Karve (Feb 17 2021 at 14:49):

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 (Feb 17 2021 at 14:50):

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 (Feb 17 2021 at 14:50):

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

#### Yakov Pechersky (Feb 17 2021 at 14:51):

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

#### Yakov Pechersky (Feb 17 2021 at 14:51):

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

Last updated: May 08 2021 at 09:11 UTC