bind

Mathlib.Control.Basic

URI: https://scilib.ai/kg/mathlib#Sum.bind

Lean4

/-- The monadic `bind` operation for `Sum`. -/
protected def bind {α β} : e ⊕ α → (α → e ⊕ β) → e ⊕ β
  | inl x, _ => inl x
  | inr x, f => f x

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

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

Разделы

Аффилиация

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