English
bind over a function mapping α to a Computation β: it acts on a sum of Computation α and Computation β by feeding the result to the next step.
Русский
Связывание по функции f: сопоставляет последовательность вычислений, отображая α в Computation β.
LaTeX
$$$\\mathrm{Bind.f} : (\\alpha \\to \\mathrm{Computation}\\, \\beta) \\to \\mathrm{Sum} (\\mathrm{Computation}\\, \\alpha) (\\mathrm{Computation}\\, \\beta) \\to \\mathrm{Sum} \\beta (\\mathrm{Sum} (\\mathrm{Computation}\\, \\alpha) (\\mathrm{Computation}\\, \\beta))$$$
Lean4
/-- bind over a function mapping `α` to a `Computation` -/
def f (f : α → Computation β) : Computation α ⊕ Computation β → β ⊕ (Computation α ⊕ Computation β)
| Sum.inl ca =>
match destruct ca with
| Sum.inl a => Bind.g <| destruct (f a)
| Sum.inr ca' => Sum.inr <| Sum.inl ca'
| Sum.inr cb => Bind.g <| destruct cb
