From b672e37bcc57c35adb97124b599fa984c52c72f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Nov 2020 08:31:34 -0800
Subject: [PATCH] chore: annotate `OfNat` and `ToString` default instances

---
 src/Init/Data/ToString/Basic.lean | 1 +
 src/Init/Prelude.lean             | 1 +
 tests/lean/run/meta7.lean         | 8 ++++++++
 3 files changed, 10 insertions(+)

diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index f6d464d233..f1a22b964d 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@@ -25,6 +25,7 @@ instance {α} [ToString α] : ToString (id α) :=
 instance {α} [ToString α] : ToString (Id α) :=
   inferInstanceAs (ToString α)
 
+@[defaultInstance]
 instance : ToString String :=
   ⟨fun s => s⟩
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 53e88bcbf3..c5b793bbb4 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -345,6 +345,7 @@ class OfNat (α : Type u) :=
 
 export OfNat (ofNat)
 
+@[defaultInstance]
 instance : OfNat Nat := ⟨id⟩
 
 instance : Inhabited Nat := {
diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean
index 7c89eade9b..0d21f1c8ac 100644
--- a/tests/lean/run/meta7.lean
+++ b/tests/lean/run/meta7.lean
@@ -167,3 +167,11 @@ def tst8 : MetaM Unit := do
   pure ()
 
 #eval tst8
+
+def tst9 : MetaM Unit := do
+  print "----- tst9 -----"
+  let defInsts ← getDefaultInstances `OfNat
+  print (toString defInsts)
+  pure ()
+
+#eval tst9