List comprehension

Stream: new members

[Burkhardt Renz]

Does Lean support syntactic sugar for list comprehension like Haskell?
If not, how to do list comprehension idiomatically in Lean?

[Edward van de Meent]

You can use docs#List.map , docs#List.foldl , docs#List.flatten and the whole shebang

[Edward van de Meent]

Alternatively, import docs#List.instMonad and use do notation

[Edward van de Meent]

Do note that unlike python and Haskell, lean does not use lazy evaluation