## 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 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 (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):

The 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