From 1f0a5233cbfb21f45f72057596cc4bc3f0254926 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 10:25:49 +0100
Subject: [PATCH] explain weird contractive_alt statement

---
 algebra/ofe.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index 0419aa3d7..a24756ca2 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -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)).
-- 
GitLab