Stream: new members
Topic: list comprehensions
Alexandre Rademaker (Jul 01 2020 at 01:43):
do we have any support for list comprehension in Lean? Something similar to Haskell with support to guards?
Bryan Gin-ge Chen (Jul 01 2020 at 01:53):
I don't think so, but you can use
def foo (n : ℕ) : list (list (ℕ × ℕ)) := do j <- list.range n, return (do i <- [1,2], return (i,j)) #eval foo 10
Alexandre Rademaker (Jul 01 2020 at 02:10):
Cool! I didn't know about the do notation. Thank you.
Alexandre Rademaker (Jul 01 2020 at 02:12):
TPinL does not mention it.
Bryan Gin-ge Chen (Jul 01 2020 at 02:14):
There's some discussion about it in chapter 6 of the Hitchhiker's guide to logical verification: https://leanprover-community.github.io/learn.html#textbooks
Last updated: May 16 2021 at 21:11 UTC