Zulip Chat Archive

Stream: new members

Topic: list comprehensions


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

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

view this post on Zulip Alexandre Rademaker (Jul 01 2020 at 02:10):

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

view this post on Zulip Alexandre Rademaker (Jul 01 2020 at 02:12):

The TPinL does not mention it.

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