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…
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…