g

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.Bind.g

← MathLib Explorer

English

The bind operation commutes with think: bind (think c) f = think (bind c f).

Русский

Связь через Think: bind (think c) f = think (bind c f).

LaTeX

$$$$ \operatorname{bind}(\mathrm{think}\,c)\ f = \mathrm{think}(\operatorname{bind} c\ f). $$$$

Lean4

/-- bind over a `Sum` of `Computation` -/
def g : β ⊕ Computation β → β ⊕ (Computation α ⊕ Computation β)
  | Sum.inl b => Sum.inl b
  | Sum.inr cb' => Sum.inr <| Sum.inr cb'

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru