Commit e7ccbf55 authored by Robbert Krebbers's avatar Robbert Krebbers

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

parents dcfb5aee 1f0a5233
......@@ -875,6 +875,7 @@ Section later.
Proper (dist n ==> dist_later n) later_car.
Proof. move=> [x] [y] /= Hxy. done. Qed.
(* f is contractive iff it can factor into `Next` and a non-expansive function. *)
Lemma contractive_alt {B : ofeT} (f : A B) :
Contractive f g : later A B,
( n, Proper (dist n ==> dist n) g) ( x, f x g (Next x)).
......
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