# Documentation

## Lake.Util.EquipT

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.

Equations
Instances For
instance Lake.instInhabitedEquipT {ρ : Type u} {m : Type v → Type w} {α : Type v} [Inhabited (m α)] :
Equations
• Lake.instInhabitedEquipT = { default := fun (x : ρ) => default }
@[inline]
def Lake.EquipT.run {ρ : Type u} {m : Type v → Type w} {α : Type v} (self : Lake.EquipT ρ m α) (r : ρ) :
m α
Equations
• self.run r = self r
Instances For
@[inline]
def Lake.EquipT.map {ρ : Type u} {m : Type v → Type w} [] {α : Type v} {β : Type v} (f : αβ) (self : Lake.EquipT ρ m α) :
Lake.EquipT ρ m β
Equations
Instances For
instance Lake.EquipT.instFunctor {ρ : Type u} {m : Type v → Type w} [] :
Equations
• Lake.EquipT.instFunctor = { map := fun {α β : Type v} => Lake.EquipT.map, mapConst := fun {α β : Type v} => Lake.EquipT.map }
@[inline]
def Lake.EquipT.pure {ρ : Type u} {m : Type v → Type w} [Pure m] {α : Type v} (a : α) :
Lake.EquipT ρ m α
Equations
Instances For
instance Lake.EquipT.instPure {ρ : Type u} {m : Type v → Type w} [Pure m] :
Pure ()
Equations
• Lake.EquipT.instPure = { pure := fun {α : Type v} => Lake.EquipT.pure }
@[inline]
def Lake.EquipT.compose {ρ : Type u} {m : Type v → Type w} {α₁ : Type v} {α₂ : Type v} {β : Type v} (f : m α₁(Unitm α₂)m β) (x₁ : Lake.EquipT ρ m α₁) (x₂ : UnitLake.EquipT ρ m α₂) :
Lake.EquipT ρ m β
Equations
Instances For
@[inline]
def Lake.EquipT.seq {ρ : Type u} {m : Type v → Type w} [Seq m] {α : Type v} {β : Type v} :
Lake.EquipT ρ m (αβ)(UnitLake.EquipT ρ m α)Lake.EquipT ρ m β
Equations
Instances For
instance Lake.EquipT.instSeq {ρ : Type u} {m : Type v → Type w} [Seq m] :
Seq ()
Equations
• Lake.EquipT.instSeq = { seq := fun {α β : Type v} => Lake.EquipT.seq }
instance Lake.EquipT.instApplicative {ρ : Type u} {m : Type v → Type w} [] :
Equations
• Lake.EquipT.instApplicative = Applicative.mk
@[inline]
def Lake.EquipT.bind {ρ : Type u} {m : Type v → Type w} [Bind m] {α : Type v} {β : Type v} (self : Lake.EquipT ρ m α) (f : αLake.EquipT ρ m β) :
Lake.EquipT ρ m β
Equations
• self.bind f fetch = do let aself fetch f a fetch
Instances For
instance Lake.EquipT.instBind {ρ : Type u} {m : Type v → Type w} [Bind m] :
Bind ()
Equations
• Lake.EquipT.instBind = { bind := fun {α β : Type v} => Lake.EquipT.bind }
instance Lake.EquipT.instMonad {ρ : Type u} {m : Type v → Type w} [] :
Equations
@[inline]
def Lake.EquipT.lift {ρ : Type u} {m : Type v → Type w} {α : Type v} (t : m α) :
Lake.EquipT ρ m α
Equations
Instances For
instance Lake.EquipT.instMonadLift {ρ : Type u} {m : Type v → Type w} :
Equations
• Lake.EquipT.instMonadLift = { monadLift := fun {α : Type v} => Lake.EquipT.lift }
instance Lake.EquipT.instMonadFunctor {ρ : Type u} {m : Type v → Type w} :
Equations
• Lake.EquipT.instMonadFunctor = { monadMap := fun {α : Type v} (f : {β : Type v} → m βm β) (x : Lake.EquipT ρ m α) (ctx : ρ) => f (x ctx) }
@[inline]
def Lake.EquipT.failure {ρ : Type u} {m : Type v → Type w} [] {α : Type v} :
Lake.EquipT ρ m α
Equations
• = failure
Instances For
@[inline]
def Lake.EquipT.orElse {ρ : Type u} {m : Type v → Type w} [] {α : Type v} :
Lake.EquipT ρ m α(UnitLake.EquipT ρ m α)Lake.EquipT ρ m α
Equations
Instances For
instance Lake.EquipT.instAlternative {ρ : Type u} {m : Type v → Type w} [] :
Equations
• Lake.EquipT.instAlternative = Alternative.mk (fun {α : Type v} => Lake.EquipT.failure) fun {α : Type v} => Lake.EquipT.orElse
@[inline]
def Lake.EquipT.throw {ρ : Type u} {m : Type v → Type w} {ε : Type v} [] {α : Type v} (e : ε) :
Lake.EquipT ρ m α
Equations
Instances For
@[inline]
def Lake.EquipT.tryCatch {ρ : Type u} {m : Type v → Type w} {ε : Type v} [] {α : Type v} (self : Lake.EquipT ρ m α) (c : εLake.EquipT ρ m α) :
Lake.EquipT ρ m α
Equations
• self.tryCatch c f = tryCatchThe ε (self f) fun (e : ε) => c e f
Instances For
instance Lake.EquipT.instMonadExceptOf {ρ : Type u} {m : Type v → Type w} (ε : Type v) [] :
Equations
• = { throw := fun {α : Type v} => Lake.EquipT.throw, tryCatch := fun {α : Type v} => Lake.EquipT.tryCatch }
@[always_inline]
instance Lake.EquipT.instMonadFinallyOfMonad {ρ : Type u} {m : Type v → Type w} [] [] :
Equations
• One or more equations did not get rendered due to their size.