is there a way to do multiple `let mut` in 1 line?

Stream: new members

[Alok Singh]

Example spelling

def f :=
  let (mut x, mut y) = (1,2)

[Philipp]

I think let mut is only allowed in do notation.

In that case the following works:

def f : Nat := Id.run do
  let mut (x, y) := (1, 2)
  x

Also see https://lean-lang.org/functional_programming_in_lean/monad-transformers/do.html?highlight=let%20mut#mutable-variables

[Alok Singh]

thanks!