diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean
index e055b36568..37f0b9e699 100644
--- a/src/Init/Lean/Elab/TermBinders.lean
+++ b/src/Init/Lean/Elab/TermBinders.lean
@@ -291,6 +291,12 @@ withLetDecl ref n type val $ fun x => do
   body ← instantiateMVars ref body;
   mkLet ref x body
 
+@[builtinTermElab «let_core»] def elabLetCore : TermElab :=
+fun stx expectedType? => match_syntax stx with
+| `(let_core $id:ident := $val; $body) =>
+   elabLetDeclAux stx id.getId #[] (mkHole stx) val body expectedType?
+| _ => throwUnsupportedSyntax
+
 def elabLetIdDecl (ref : Syntax) (decl body : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
 -- `decl` is of the form: ident bracktedBinder+ (`:` term)? `:=` term
 let n        := decl.getIdAt 0;
diff --git a/tests/lean/run/macroid.lean b/tests/lean/run/macroid.lean
index 7a4a82eb21..e83296cce3 100644
--- a/tests/lean/run/macroid.lean
+++ b/tests/lean/run/macroid.lean
@@ -11,3 +11,5 @@ macro_rules
 | `(case! $h : $cond with $t, $e) => `((fun $h => cond $h $t $e) $cond)
 
 #check case! h : 0 == 0 with h, not h
+
+#check let_core x := 1+2; x+x