Commit 558b080f authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coq

parents eb8b5c60 62e8a98b
This diff is collapsed.
......@@ -183,10 +183,15 @@ Section ofe.
transitivity (c n); first by apply conv_compl. symmetry.
apply chain_cauchy. omega.
Qed.
Lemma timeless_iff n (x : A) `{!Timeless x} y : x y x {n} y.
Proof.
split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
Qed.
Lemma timeless_iff_0 n (x : A) `{!Timeless x} y : x {0} y x {n} y.
Proof.
split=> ?. by apply equiv_dist, (timeless _). eauto using dist_le with lia.
Qed.
End ofe.
(** Contractive functions *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment