From 68701b86e4032729ad36d655a809a2feb192d41e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Dec 2020 14:32:49 -0800
Subject: [PATCH] feat: add `Repr Name`

---
 src/Init/Meta.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a86cf9928a..da95e2a864 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -49,7 +49,11 @@ def toStringWithSep (sep : String) : Name → String
 protected def toString : Name → String :=
   toStringWithSep "."
 
-instance : ToString Name := ⟨Name.toString⟩
+instance : ToString Name where
+  toString n := n.toString
+
+instance : Repr Name where
+  reprPrec n _ := Std.Format.text "`" ++ n.toString
 
 def capitalize : Name → Name
   | Name.str p s _ => Name.mkStr p s.capitalize