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

• Lake.EquipT ρ m α = (ρ → m α)

@[inline]

def Lake.EquipT.mk {ρ : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} (x : ρ → m α) : EquipT ρ m α

Equations

• Lake.EquipT.mk x = x

@[instance_reducible]

instance Lake.EquipT.instInhabited {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Inhabited (m α)] : Inhabited (EquipT ρ m α)

Equations

• Lake.EquipT.instInhabited = { default := Lake.EquipT.mk fun (x : ρ) => default }

@[inline]

def Lake.EquipT.run {ρ : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} (self : EquipT ρ m α) (r : ρ) : m α

Equations

• self.run r = self r

@[inline]

def Lake.EquipT.map {m : Type u_1 → Type u_2} {α β : Type u_1} {ρ : Type u_3} [Functor m] (f : α → β) (self : EquipT ρ m α) : EquipT ρ m β

Equations

• Lake.EquipT.map f self r = f <$> self r

@[instance_reducible]

instance Lake.EquipT.instFunctor {m : Type u_1 → Type u_2} {ρ : Type u_3} [Functor m] : Functor (EquipT ρ m)

Equations

• Lake.EquipT.instFunctor = { map := fun {α β : Type ?u.3} => Lake.EquipT.map }

@[inline]

def Lake.EquipT.pure {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_3} [Pure m] (a : α) : EquipT ρ m α

Equations

• Lake.EquipT.pure a x✝ = pure a

@[instance_reducible]

instance Lake.EquipT.instPure {m : Type u_1 → Type u_2} {ρ : Type u_3} [Pure m] : Pure (EquipT ρ m)

Equations

• Lake.EquipT.instPure = { pure := fun {α : Type ?u.3} => Lake.EquipT.pure }

@[inline]

def Lake.EquipT.compose {m : Type u_1 → Type u_2} {ρ : Type u_3} {α₁ α₂ β : Type u_1} (f : m α₁ → (Unit → m α₂) → m β) (x₁ : EquipT ρ m α₁) (x₂ : Unit → EquipT ρ m α₂) : EquipT ρ m β

Equations

• Lake.EquipT.compose f x₁ x₂ r = f (x₁ r) fun (x : Unit) => x₂ () r

@[inline]

def Lake.EquipT.seq {m : Type u_1 → Type u_2} {ρ : Type u_3} {α β : Type u_1} [Seq m] : EquipT ρ m (α → β) → (Unit → EquipT ρ m α) → EquipT ρ m β

Equations

• Lake.EquipT.seq = Lake.EquipT.compose Seq.seq

@[instance_reducible]

instance Lake.EquipT.instSeq {m : Type u_1 → Type u_2} {ρ : Type u_3} [Seq m] : Seq (EquipT ρ m)

Equations

• Lake.EquipT.instSeq = { seq := fun {α β : Type ?u.3} => Lake.EquipT.seq }

@[instance_reducible]

instance Lake.EquipT.instApplicative {m : Type u_1 → Type u_2} {ρ : Type u_3} [Applicative m] : Applicative (EquipT ρ m)

Equations

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

@[inline]

def Lake.EquipT.bind {m : Type u_1 → Type u_2} {ρ : Type u_3} {α β : Type u_1} [Bind m] (self : EquipT ρ m α) (f : α → EquipT ρ m β) : EquipT ρ m β

Equations

• self.bind f r = do let a ← self r f a r

@[instance_reducible]

instance Lake.EquipT.instBind {m : Type u_1 → Type u_2} {ρ : Type u_3} [Bind m] : Bind (EquipT ρ m)

Equations

• Lake.EquipT.instBind = { bind := fun {α β : Type ?u.3} => Lake.EquipT.bind }

@[instance_reducible]

instance Lake.EquipT.instMonad {m : Type u_1 → Type u_2} {ρ : Type u_3} [Monad m] : Monad (EquipT ρ m)

Equations

• Lake.EquipT.instMonad = { toApplicative := Lake.EquipT.instApplicative, toBind := Lake.EquipT.instBind }

@[inline]

def Lake.EquipT.lift {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} (t : m α) : EquipT ρ m α

Equations

• Lake.EquipT.lift t x✝ = t

@[instance_reducible]

instance Lake.EquipT.instMonadLift {m : Type u_1 → Type u_2} {ρ : Type u_3} : MonadLift m (EquipT ρ m)

Equations

• Lake.EquipT.instMonadLift = { monadLift := fun {α : Type ?u.3} => Lake.EquipT.lift }

@[instance_reducible]

instance Lake.EquipT.instMonadFunctor {m : Type u_1 → Type u_2} {ρ : Type u_3} : MonadFunctor m (EquipT ρ m)

Equations

• Lake.EquipT.instMonadFunctor = { monadMap := fun {α : Type ?u.3} (f : {β : Type ?u.3} → m β → m β) (x : Lake.EquipT ρ m α) => Lake.EquipT.mk fun (ctx : ρ) => f (x.run ctx) }

@[inline]

def Lake.EquipT.failure {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Alternative m] : EquipT ρ m α

Equations

• Lake.EquipT.failure x✝ = failure

@[inline]

def Lake.EquipT.orElse {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Alternative m] : EquipT ρ m α → (Unit → EquipT ρ m α) → EquipT ρ m α

Equations

• Lake.EquipT.orElse = Lake.EquipT.compose Alternative.orElse

@[instance_reducible]

instance Lake.EquipT.instAlternative {m : Type u_1 → Type u_2} {ρ : Type u_3} [Alternative m] : Alternative (EquipT ρ m)

Equations

• Lake.EquipT.instAlternative = { toApplicative := Lake.EquipT.instApplicative, failure := fun {α : Type ?u.3} => Lake.EquipT.failure, orElse := fun {α : Type ?u.3} => Lake.EquipT.orElse }

@[inline]

def Lake.EquipT.throw {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ : Type u_4} {α : Type u_2} [MonadExceptOf ε m] (e : ε) : EquipT ρ m α

Equations

• Lake.EquipT.throw e x✝ = throw e

@[inline]

def Lake.EquipT.tryCatch {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ : Type u_4} {α : Type u_2} [MonadExceptOf ε m] (self : EquipT ρ m α) (c : ε → EquipT ρ m α) : EquipT ρ m α

Equations

• self.tryCatch c f = tryCatchThe ε (self f) fun (e : ε) => c e f

@[instance_reducible]

instance Lake.EquipT.instMonadExceptOf {m : Type u_1 → Type u_2} {ρ : Type u_3} (ε : Type u_4) [MonadExceptOf ε m] : MonadExceptOf ε (EquipT ρ m)

Equations

• Lake.EquipT.instMonadExceptOf ε = { throw := fun {α : Type ?u.4} => Lake.EquipT.throw, tryCatch := fun {α : Type ?u.4} => Lake.EquipT.tryCatch }

@[inline]

def Lake.EquipT.tryFinally' {m : Type (max u_1 u_2) → Type u_3} {ρ : Type u_4} {α β : Type (max u_1 u_2)} [MonadFinally m] [Monad m] (x : EquipT ρ m α) (f : Option α → EquipT ρ m β) : EquipT ρ m (α × β)

Equations

• x.tryFinally' f ctx = tryFinally' (x.run ctx) fun (a? : Option α) => (f a?).run ctx

@[instance_reducible]

instance Lake.EquipT.instMonadFinallyOfMonad {m : Type (max u_1 u_2) → Type u_3} {ρ : Type u_4} [MonadFinally m] [Monad m] : MonadFinally (EquipT ρ m)

Equations

• Lake.EquipT.instMonadFinallyOfMonad = { tryFinally' := fun {α β : Type (max ?u.4 ?u.3)} => Lake.EquipT.tryFinally' }