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