Documentation

Lake.Util.Lift

instance Lake.instMonadLiftTId {m : Type u_1 → Type u_2} [Pure m] :
Equations
  • Lake.instMonadLiftTId = { monadLift := fun {α} act => pure (Id.run act) }
Equations
  • Lake.instMonadLiftTOption = { monadLift := fun {α} x => 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] :
Equations
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] :
Equations
  • Lake.instMonadLiftTReaderT = { monadLift := fun {α} act => 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] :
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] :
Equations
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] :
Equations
instance Lake.instMonadLiftTEIO {m : TypeType u_1} {ε : Type} [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] :
Equations
Equations