From b510bb305d593008631193c4e22456365161b6b5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Oct 2021 16:12:50 -0700
Subject: [PATCH] feat: elaborate `let_mvar%`

---
 src/Lean/Elab/BuiltinTerm.lean | 12 ++++++++++++
 tests/lean/run/letMVar.lean    |  8 ++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 tests/lean/run/letMVar.lean

diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 6157a9ecfc..1ddc3aff18 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -95,6 +95,18 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
         else
           throwError "synthetic hole has already been defined with an incompatible local context"
 
+@[builtinTermElab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(let_mvar% ? $n := $e; $b) =>
+     match (← getMCtx).findUserName? n.getId with
+     | some _ => throwError "invalid 'let_mvar%', metavariable '?{n.getId}' has already been used"
+     | none =>
+       let e ← elabTerm e none
+       let mvar ← mkFreshExprMVar (← inferType e) MetavarKind.syntheticOpaque n.getId
+       assignExprMVar mvar.mvarId! e
+       elabTerm b expectedType?
+  | _ => throwUnsupportedSyntax
+
 private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
   let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
   let mvarId := mvar.mvarId!
diff --git a/tests/lean/run/letMVar.lean b/tests/lean/run/letMVar.lean
new file mode 100644
index 0000000000..096ffb79ab
--- /dev/null
+++ b/tests/lean/run/letMVar.lean
@@ -0,0 +1,8 @@
+def tst (x : Nat) : Nat :=
+  let_mvar% ?m := x + 1;
+  ?m + ?m
+
+#print tst
+
+example : tst x = (x + 1) + (x + 1) :=
+  rfl