Zulip Chat Archive

Stream: new members

Topic: list of natural numbers


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 17 2021 at 14:50):

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

view this post on Zulip Yakov Pechersky (Feb 17 2021 at 14:51):

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

view this post on Zulip 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