From e7f379fb0fd02e3dcd84f37fd4244b8f2bf090c1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Apr 2019 11:54:33 -0700
Subject: [PATCH] chore(library/init/control/id): spurious `[inline]`
 annotations

---
 library/init/control/id.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/init/control/id.lean b/library/init/control/id.lean
index 604bd3bdf0..95d289a03d 100644
--- a/library/init/control/id.lean
+++ b/library/init/control/id.lean
@@ -20,11 +20,11 @@ f x
 @[inline] def Id.map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
 f x
 
-@[inline] instance : Monad Id :=
+instance : Monad Id :=
 { pure := @Id.pure, bind := @Id.bind, map := @Id.map }
 
 @[inline] def Id.run {α : Type u} (x : Id α) : α :=
 x
 
-@[inline] instance : MonadRun id Id :=
+instance : MonadRun id Id :=
 ⟨@Id.run⟩