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