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

[Agnishom Chattopadhyay]

It seems that I have to import Mathlib.Init.Data.List.Instances in order for this to work? Why isn't the monad instance for lists included by default?

[Alex J. Best]

Everything has to live somewhere, so what do you mean by "by default" the only things included in prelude are really the bare essentials to get the system off the ground, nothing more. And it turns out the monad isntance for lists is not really used that widely either.
I recommend using import Mathlib while developing / searching for instanes.