From 019314db1f52e4e3e7ab5240c1bff62c62815d4d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 16 Jun 2019 23:00:31 +0200
Subject: [PATCH] Comment about the relation between `discrete_fun` and
 non-expansive functions.

---
 theories/algebra/ofe.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c84bced7c..61dc56986 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1103,9 +1103,12 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply oFunctor_ne, Hfg.
 Qed.
 
-(* Dependently-typed functions over a discrete domain *)
-(* We make [discrete_fun] a definition so that we can register it as a canonical
-structure. *)
+(** Dependently-typed functions over a discrete domain *)
+(** We make [discrete_fun] a definition so that we can register it as a
+canonical structure. Note that non-dependent functions over a discrete domain,
+[discrete_fun (λ _, A) B] (or [A -d> B] following the notation we introduce
+below) are isomorphic to [leibnizC A -n> B]. In other words, since the domain
+is discrete, we get non-expansiveness for free. *)
 Definition discrete_fun {A} (B : A → ofeT) := ∀ x : A, B x.
 
 Section discrete_fun.
-- 
GitLab