From 9f69991d808ffe21b576fea2ed66eea6ac18d62d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jan 2020 13:30:11 -0800
Subject: [PATCH] feat: elaborate `show` notation

---
 src/Init/Lean/Elab/BuiltinNotation.lean | 5 +++++
 tests/lean/run/frontend1.lean           | 2 ++
 2 files changed, 7 insertions(+)

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"