Theorems · Theorem · logic and foundations

Computation.results_bind

∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β} {m n : ℕ},
  s.Results a m → (f a).Results b n → (s.bind f).Results b (n + m)

Defined in

Mathlib.Data.Seq.Computation

Cited by

2 results in Mathlib

Foundations

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