Zulip Chat Archive
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: Dec 20 2023 at 11:08 UTC