instance Lake.instMonadLiftTId {m : Type u_1 → Type u_2} [Pure m] : MonadLiftT Id m

Equations

• Lake.instMonadLiftTId = { monadLift := fun {α : Type u_1} (act : Id α) => pure (Id.run act) }

instance Lake.instMonadLiftTOption {m : Type u_1 → Type u_2} [Alternative m] : MonadLiftT Option m

Equations

• Lake.instMonadLiftTOption = { monadLift := fun {α : Type u_1} (x : Option α) => match x with | some a => pure a | none => failure }

instance Lake.instMonadLiftTExcept {m : Type u_1 → Type u_2} {ε : Type u_3} [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m

Equations

• Lake.instMonadLiftTExcept = { monadLift := fun {α : Type u_1} (x : Except ε α) => match x with | Except.ok a => pure a | Except.error e => throw e }

instance Lake.instMonadLiftTReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} {n : Type u_1 → Type u_3} [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m

Equations

• Lake.instMonadLiftTReaderT = { monadLift := fun {α : Type u_1} (act : ReaderT ρ n α) => do let __do_lift ← read liftM (act __do_lift) }

instance Lake.instMonadLiftTStateT {m : Type u_1 → Type u_2} {σ : Type u_1} {n : Type u_1 → Type u_3} [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m

Equations

• One or more equations did not get rendered due to their size.

instance Lake.instMonadLiftTOptionT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m

Equations

• Lake.instMonadLiftTOptionT = { monadLift := fun {α : Type u_1} (act : OptionT n α) => liftM (OptionT.run act) >>= liftM }

instance Lake.instMonadLiftTExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {n : Type u_1 → Type u_3} [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m

Equations

• Lake.instMonadLiftTExceptT = { monadLift := fun {α : Type u_1} (act : ExceptT ε n α) => liftM (ExceptT.run act) >>= liftM }

instance Lake.instMonadLiftTEIO {m : Type → Type u_1} {ε : Type} [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m

Equations

• Lake.instMonadLiftTEIO = { monadLift := fun {α : Type} (act : EIO ε α) => liftM (EIO.toBaseIO act) >>= liftM }

instance Lake.instMonadLiftTOptionIO {m : Type → Type u_1} [Monad m] [Alternative m] [MonadLiftT BaseIO m] : MonadLiftT Lake.OptionIO m

Equations

• Lake.instMonadLiftTOptionIO = { monadLift := fun {α : Type} (act : Lake.OptionIO α) => liftM (Lake.OptionIO.toBaseIO act) >>= liftM }