instance
Lake.instInhabitedEquipT
{ρ : Type u}
{m : Type v → Type w}
{α : Type v}
[Inhabited (m α)]
:
Inhabited (Lake.EquipT ρ m α)
@[inline]
def
Lake.EquipT.run
{ρ : Type u}
{m : Type v → Type w}
{α : Type v}
(self : Lake.EquipT ρ m α)
(r : ρ)
:
m α
Instances For
@[inline]
def
Lake.EquipT.map
{ρ : Type u}
{m : Type v → Type w}
[Functor m]
{α : Type v}
{β : Type v}
(f : α → β)
(self : Lake.EquipT ρ m α)
:
Lake.EquipT ρ m β
Instances For
instance
Lake.EquipT.instFunctorEquipT
{ρ : Type u}
{m : Type v → Type w}
[Functor m]
:
Functor (Lake.EquipT ρ m)
@[inline]
def
Lake.EquipT.pure
{ρ : Type u}
{m : Type v → Type w}
[Pure m]
{α : Type v}
(a : α)
:
Lake.EquipT ρ m α
Instances For
instance
Lake.EquipT.instPureEquipT
{ρ : Type u}
{m : Type v → Type w}
[Pure m]
:
Pure (Lake.EquipT ρ m)
@[inline]
def
Lake.EquipT.compose
{ρ : Type u}
{m : Type v → Type w}
{α₁ : Type v}
{α₂ : Type v}
{β : Type v}
(f : m α₁ → (Unit → m α₂) → m β)
(x₁ : Lake.EquipT ρ m α₁)
(x₂ : Unit → Lake.EquipT ρ m α₂)
:
Lake.EquipT ρ m β
Instances For
@[inline]
def
Lake.EquipT.seq
{ρ : Type u}
{m : Type v → Type w}
[Seq m]
{α : Type v}
{β : Type v}
:
Lake.EquipT ρ m (α → β) → (Unit → Lake.EquipT ρ m α) → Lake.EquipT ρ m β
Instances For
instance
Lake.EquipT.instSeqEquipT
{ρ : Type u}
{m : Type v → Type w}
[Seq m]
:
Seq (Lake.EquipT ρ m)
instance
Lake.EquipT.instApplicativeEquipT
{ρ : Type u}
{m : Type v → Type w}
[Applicative m]
:
Applicative (Lake.EquipT ρ m)
@[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 β
Instances For
instance
Lake.EquipT.instBindEquipT
{ρ : Type u}
{m : Type v → Type w}
[Bind m]
:
Bind (Lake.EquipT ρ m)
instance
Lake.EquipT.instMonadEquipT
{ρ : Type u}
{m : Type v → Type w}
[Monad m]
:
Monad (Lake.EquipT ρ m)
@[inline]
Instances For
instance
Lake.EquipT.instMonadLiftEquipT
{ρ : Type u}
{m : Type v → Type w}
:
MonadLift m (Lake.EquipT ρ m)
@[inline]
def
Lake.EquipT.failure
{ρ : Type u}
{m : Type v → Type w}
[Alternative m]
{α : Type v}
:
Lake.EquipT ρ m α
Instances For
@[inline]
def
Lake.EquipT.orElse
{ρ : Type u}
{m : Type v → Type w}
[Alternative m]
{α : Type v}
:
Lake.EquipT ρ m α → (Unit → Lake.EquipT ρ m α) → Lake.EquipT ρ m α
Instances For
instance
Lake.EquipT.instAlternativeEquipT
{ρ : Type u}
{m : Type v → Type w}
[Alternative m]
:
Alternative (Lake.EquipT ρ m)
@[inline]
def
Lake.EquipT.throw
{ρ : Type u}
{m : Type v → Type w}
{ε : Type v}
[MonadExceptOf ε m]
{α : Type v}
(e : ε)
:
Lake.EquipT ρ m α
Instances For
@[inline]
def
Lake.EquipT.tryCatch
{ρ : Type u}
{m : Type v → Type w}
{ε : Type v}
[MonadExceptOf ε m]
{α : Type v}
(self : Lake.EquipT ρ m α)
(c : ε → Lake.EquipT ρ m α)
:
Lake.EquipT ρ m α
Instances For
instance
Lake.EquipT.instMonadExceptOfEquipT
{ρ : Type u}
{m : Type v → Type w}
(ε : Type v)
[MonadExceptOf ε m]
:
MonadExceptOf ε (Lake.EquipT ρ m)