From f39b1b837852a4cd5bdafc1fe5f58a608d17dcc6 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 14 Sep 2021 11:18:16 -0400
Subject: [PATCH] chore: remove unused `MonadLiftT Id` instance

---
 Lake/BuildMonad.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Lake/BuildMonad.lean b/Lake/BuildMonad.lean
index 2dc6ea3e1a..bf5e3cd7b8 100644
--- a/Lake/BuildMonad.lean
+++ b/Lake/BuildMonad.lean
@@ -52,9 +52,6 @@ end BuildMethodsRef
 -- # Build Monad Utilities
 --------------------------------------------------------------------------------
 
--- Ideally, this instance would be in the Lean core
-instance [Pure m] : MonadLiftT Id m := ⟨pure⟩
-
 namespace BuildContext
 
 deriving instance Inhabited for BuildContext