Concise syntax for mutating variables in a do block.

Stream: Is there code for X?

[Asei Inoue]

I am trying to create a library that allows a concise procedural language-like writing style when overwriting the value of a variable in a do block.

import Lean

/-! ### Addition -/

syntax ident "+=" term : doElem

macro_rules
  | `(doElem| $x:ident += $e:term) => `(doElem| ($x) := ($x) + ($e))

#eval do
  let mut l : Nat := 0
  l += 2
  l += 3
  IO.println l
  let check := l = 5
  if not check then
    IO.throwServerError "error"

/-! ### Subtraction -/

syntax ident "-=" term : doElem

macro_rules
  | `(doElem| $x:ident -= $e:term) => `(doElem| ($x) := ($x) - ($e))

#eval do
  let mut l : Nat := 5
  l -= 2
  l -= 3
  IO.println l
  let check := l = 0
  if not check then
    IO.throwServerError "error"

/-! ### List concatenation -/

syntax ident "++=" term : doElem

macro_rules
  | `(doElem| $x:ident ++= $e:term) => `(doElem| ($x) := ($x) ++ ($e))

#eval do
  let mut l : List Nat := []
  l ++= [1, 1]
  l ++= [2, 3, 5]
  IO.println l
  let check := l = [1, 1, 2, 3, 5]
  if not check then
    IO.throwServerError "error"

However, I am stuck on the syntax for mutating arrays and lists. array[i]! := y, which I thought would be a good shorthand for array := array.set! i y, but I would like to hear what others have to say. What syntax would you suggest?