list comprehensions

Stream: new members

[Alexandre Rademaker]

do we have any support for list comprehension in Lean? Something similar to Haskell with support to guards?

[Bryan Gin-ge Chen]

I don't think so, but you can use do notation:

def foo (n : ℕ) : list (list (ℕ × ℕ)) :=
do j <- list.range n,
   return (do i <- [1,2],
              return (i,j))

#eval foo 10

[Alexandre Rademaker]

Cool! I didn't know about the do notation. Thank you.

[Alexandre Rademaker]

The TPinL does not mention it.

[Bryan Gin-ge Chen]

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