From 8985a15f9647542f35aa623bc1ded2bb0b4a3fa0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Aug 2022 19:08:51 -0700
Subject: [PATCH] chore: mark `inferInstance` and `inferInstanceAs` as
 `[inline]`

New code generator does not inline simple declarations not tagged with
`[inline]` yet. We need this change to simpilify testing
---
 src/Init/Prelude.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 1e77419d6e..4dd1611208 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -83,7 +83,7 @@ example : foo.default = (default, default) :=
   rfl
 ```
 -/
-@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
+abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
 /-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
@@ -97,7 +97,7 @@ does.) Example:
 #check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
 ```
 -/
-@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i
+abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
 
 set_option bootstrap.inductiveCheckResultingUniverse false in
 /--