Theorems · Theorem · logic and foundations

Computation.liftRel_bind

∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
  {s2 : Computation β} {f1 : α → Computation γ} {f2 : β → Computation δ},
  Computation.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → Computation.LiftRel S (f1 a) (f2 b)) → Computation.LiftRel S (s1.bind f1) (s2.bind f2)

Defined in

Mathlib.Data.Seq.Computation

Cited by

5 results in Mathlib

Foundations

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