Theorems · Theorem · logic and foundations

Computation.of_results_bind

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

Defined in

Mathlib.Data.Seq.Computation

Cited by

2 results in Mathlib

Foundations

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