diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 890fd6c83d..7f8e56c19a 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -637,6 +637,13 @@ fun stx expectedType? => do
 @[builtinTermElab explicit] def elabExplicit : TermElab := elabApp
 @[builtinTermElab choice] def elabChoice : TermElab := elabApp
 
+@[builtinTermElab dollar] def elabDollar : TermElab :=
+fun stx expectedType? => do
+  -- term `$` term
+  let f := stx.getArg 0;
+  let a := stx.getArg 2;
+  elabTerm (mkAppStx f #[a]) expectedType?
+
 end Term
 
 @[init] private def regTraceClasses : IO Unit := do
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index f2b776a898..a2700f19e7 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -20,6 +20,7 @@ def two := 2
 -- set_option trace.Elab true
 
 #eval run "#check [zero, one, two]"
+#eval run "#check id $ Nat.succ one"
 
 #eval run
 "universe u universe v