Elaboration failure with let mut whose RHS is a do notation

Stream: lean4

[Siddharth Bhat]

Consider the MWE:

def fails : MetaM Unit := do
  let mut val : Bool ← do
      pure true
  -- unknown identifier val
  val := Bool.not val -- FAILS!
  return ()

def succeeds : MetaM Unit := do
  let val : Bool ← do
      pure true
  let mut val := val
  val := Bool.not val
  return ()

Does someone know what I'm doing wrong here?

[Mario Carneiro]

this is a bug in the do notation

[Siddharth Bhat]

OK, let me file a bug.

[Siddharth Bhat]

Filed: https://github.com/leanprover/lean4/issues/5607