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 ""⟩