diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index c3d395fbf7..3d55c4c6dd 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -55,6 +55,11 @@ match expectedType? with
     | _ => throwError ref ("invalid constructor ⟨...⟩, '" ++ constName ++ "' is not an inductive type")
   | _ => throwError ref ("invalid constructor ⟨...⟩, expected type is not an inductive type " ++ indentExpr expectedType)
 
+@[builtinTermElab «show»] def elabShow : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
+| _                       => unreachable!
+
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
   -- term `op` term
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 8dc94cd8be..baa6b27617 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -185,3 +185,5 @@ f a
 #eval run "#check fun (i : Nat) (a : Array Nat) => if h : i < a.size then a.get ⟨i, h⟩ else i"
 #eval run "#check Prod.fst ⟨1, 2⟩"
 #eval run "#check let x := ⟨1, 2⟩; Prod.fst x"
+#eval run "#check show Nat from 1"
+#eval run "#check show Int from 1"