That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement. The nice thi

That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement. The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations. Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.