eric-wieser

Mathlib4 provides a `Monad List` instance, which you can see at https://leanprover-community.github.io/mathlib4_docs/Mathlib...

It has the following which means the same as what you wrote:

    do let x ← List.range' 1 10; return x^2

The syntax is flexible enough that you could build your own:

    macro "[" r:term "|" preamble:doElem "]" : term => `(do 
    $preamble; return $r)

    #eval [x^2 | let x ← List.range' 1 10]