Theorems · Theorem · logic and foundations

Computation.bind_assoc

∀ {α : Type u} {β : Type v} {γ : Type w} (s : Computation α) (f : α → Computation β) (g : β → Computation γ),
  (s.bind f).bind g = s.bind fun x => (f x).bind g

Defined in

Mathlib.Data.Seq.Computation

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound