From fdf4deedaffc678a9bb7cd72bb96412c0ff3c40e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 25 Jul 2021 12:53:25 +0200
Subject: [PATCH] Tests for non-expansive of uncurry.

---
 tests/algebra.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/tests/algebra.v b/tests/algebra.v
index 39e569f17..99d7b0f71 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -68,3 +68,16 @@ Definition auth_check {A : ucmra} :
   auth A = authO A := eq_refl.
 Definition gmap_view_check {K : Type} `{Countable K} {V : ofe} :
   gmap_view K V = gmap_viewO K V := eq_refl.
+
+Lemma uncurry_ne_test {A B C : ofe} (f : A → B → C) :
+  (∀ n, Proper (dist n ==> dist n ==> dist n) f) →
+  NonExpansive (uncurry f).
+Proof. apply _. Qed.
+Lemma uncurry3_ne_test {A B C D : ofe} (f : A → B → C → D) :
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f) →
+  NonExpansive (uncurry3 f).
+Proof. apply _. Qed.
+Lemma uncurry4_ne_test {A B C D E : ofe} (f : A → B → C → D → E) :
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f) →
+  NonExpansive (uncurry4 f).
+Proof. apply _. Qed.
-- 
GitLab