From 052d6623f0e9ca0d56b7e16b372e7512a42350a5 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 3 Dec 2021 17:44:57 -0500
Subject: [PATCH] refactor: move misc utilities to `Util.Extra`

---
 Lake/Util/Async.lean |  8 +-------
 Lake/Util/Misc.lean  | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 7 deletions(-)
 create mode 100644 Lake/Util/Misc.lean

diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean
index 91f7116fe0..4cfb2f90e0 100644
--- a/Lake/Util/Async.lean
+++ b/Lake/Util/Async.lean
@@ -5,16 +5,10 @@ Authors: Mac Malone
 -/
 import Lake.Util.Task
 import Lake.Util.OptionIO
+import Lake.Util.Misc
 
 namespace Lake
 
-def liftOption [Alternative m] : Option α → m α
-| some a => pure a
-| none => failure
-
-instance [MonadLift m n] : MonadLift (ReaderT ρ m) (ReaderT ρ n) where
-  monadLift x := fun r => liftM <| x r
-
 --------------------------------------------------------------------------------
 -- # Async / Await Abstraction
 --------------------------------------------------------------------------------
diff --git a/Lake/Util/Misc.lean b/Lake/Util/Misc.lean
new file mode 100644
index 0000000000..ee9ca4d754
--- /dev/null
+++ b/Lake/Util/Misc.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+def liftOption [Alternative m] : Option α → m α
+| some a => pure a
+| none => failure
+
+instance [MonadLiftT m n] : MonadLiftT (ReaderT ρ m) (ReaderT ρ n) where
+  monadLift x := fun r => liftM <| x r