def Lake.EquipT (ρ : Type u) (m : Type v → Type w) (α : Type v) : Type (max u w)

A monad transformer that equips a monad with a value. This is a generalization of ReaderT where the value is not necessarily directly readable through the monad.

instance Lake.instInhabitedEquipT {ρ : Type u} {m : Type v → Type w} {α : Type v} [Inhabited (m α)] : Inhabited (EquipT ρ m α)

@[inline]

def Lake.EquipT.run {ρ : Type u} {m : Type v → Type w} {α : Type v} (self : EquipT ρ m α) (r : ρ) : m α

@[inline]

def Lake.EquipT.map {ρ : Type u} {m : Type v → Type w} [Functor m] {α β : Type v} (f : α → β) (self : EquipT ρ m α) : EquipT ρ m β

instance Lake.EquipT.instFunctor {ρ : Type u} {m : Type v → Type w} [Functor m] : Functor (EquipT ρ m)

@[inline]

def Lake.EquipT.pure {ρ : Type u} {m : Type v → Type w} [Pure m] {α : Type v} (a : α) : EquipT ρ m α

instance Lake.EquipT.instPure {ρ : Type u} {m : Type v → Type w} [Pure m] : Pure (EquipT ρ m)

@[inline]

def Lake.EquipT.compose {ρ : Type u} {m : Type v → Type w} {α₁ α₂ β : Type v} (f : m α₁ → (Unit → m α₂) → m β) (x₁ : EquipT ρ m α₁) (x₂ : Unit → EquipT ρ m α₂) : EquipT ρ m β

@[inline]

def Lake.EquipT.seq {ρ : Type u} {m : Type v → Type w} [Seq m] {α β : Type v} : EquipT ρ m (α → β) → (Unit → EquipT ρ m α) → EquipT ρ m β

instance Lake.EquipT.instSeq {ρ : Type u} {m : Type v → Type w} [Seq m] : Seq (EquipT ρ m)

instance Lake.EquipT.instApplicative {ρ : Type u} {m : Type v → Type w} [Applicative m] : Applicative (EquipT ρ m)

@[inline]

def Lake.EquipT.bind {ρ : Type u} {m : Type v → Type w} [Bind m] {α β : Type v} (self : EquipT ρ m α) (f : α → EquipT ρ m β) : EquipT ρ m β

instance Lake.EquipT.instBind {ρ : Type u} {m : Type v → Type w} [Bind m] : Bind (EquipT ρ m)

instance Lake.EquipT.instMonad {ρ : Type u} {m : Type v → Type w} [Monad m] : Monad (EquipT ρ m)

@[inline]

def Lake.EquipT.lift {ρ : Type u} {m : Type v → Type w} {α : Type v} (t : m α) : EquipT ρ m α

instance Lake.EquipT.instMonadLift {ρ : Type u} {m : Type v → Type w} : MonadLift m (EquipT ρ m)

instance Lake.EquipT.instMonadFunctor {ρ : Type u} {m : Type v → Type w} : MonadFunctor m (EquipT ρ m)

@[inline]

def Lake.EquipT.failure {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} : EquipT ρ m α

@[inline]

def Lake.EquipT.orElse {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} : EquipT ρ m α → (Unit → EquipT ρ m α) → EquipT ρ m α

instance Lake.EquipT.instAlternative {ρ : Type u} {m : Type v → Type w} [Alternative m] : Alternative (EquipT ρ m)

@[inline]

def Lake.EquipT.throw {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (e : ε) : EquipT ρ m α

@[inline]

def Lake.EquipT.tryCatch {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (self : EquipT ρ m α) (c : ε → EquipT ρ m α) : EquipT ρ m α

instance Lake.EquipT.instMonadExceptOf {ρ : Type u} {m : Type v → Type w} (ε : Type v) [MonadExceptOf ε m] : MonadExceptOf ε (EquipT ρ m)

@[always_inline]

instance Lake.EquipT.instMonadFinallyOfMonad {ρ : Type u} {m : Type v → Type w} [MonadFinally m] [Monad m] : MonadFinally (EquipT ρ m)