feat: elaborate show notation

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

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"