diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 01b4335bd3..a70a3fbbdd 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -27,7 +27,6 @@ instance {α} [ToString α] : ToString (id α) := instance {α} [ToString α] : ToString (Id α) := inferInstanceAs (ToString α) -@[defaultInstance low] instance : ToString String := ⟨fun s => s⟩