Theorems · Definition · logic and foundations

Computation.LiftRel

{α : Type u} → {β : Type v} → (α → β → Prop) → Computation α → Computation β → Prop

LiftRel R ca cb is a generalization of Equiv to relations other than equality. It asserts that if ca terminates with a, then cb terminates with some b such that R a b, and if cb terminates with b then ca terminates with some a such that R a b.

Defined in

Mathlib.Data.Seq.Computation

Cited by

38 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms