From 7c8fcb3233e8279c8e5638775beeec4a3fbaaf2d Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 30 Sep 2022 10:21:44 +0100 Subject: [PATCH] fix: rm instance TypeName String because it is unused --- src/Lean/Elab/Deriving/TypeName.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean index de36124868..17a0cc896a 100644 --- a/src/Lean/Elab/Deriving/TypeName.lean +++ b/src/Lean/Elab/Deriving/TypeName.lean @@ -23,6 +23,3 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool initialize registerDerivingHandler ``TypeName deriveTypeNameInstance - -deriving instance TypeName for String -instance : Inhabited Dynamic := ⟨Dynamic.mk ""⟩