From 7607c53e9132d2fe3adb7520909573bcfae56098 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 25 Jul 2021 12:58:13 +0200
Subject: [PATCH] Similar tests for `curry`.

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

diff --git a/tests/algebra.v b/tests/algebra.v
index 99d7b0f71..23edb9038 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -81,3 +81,16 @@ 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.
+
+Lemma curry_ne_test {A B C : ofe} (f : A * B → C) :
+  NonExpansive f →
+  ∀ n, Proper (dist n ==> dist n ==> dist n) (curry f).
+Proof. apply _. Qed.
+Lemma curry3_ne_test {A B C D : ofe} (f : A * B * C → D) :
+  NonExpansive f →
+  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) (curry3 f).
+Proof. apply _. Qed.
+Lemma curry4_ne_test {A B C D E : ofe} (f : A * B * C * D → E) :
+  NonExpansive f →
+  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (curry4 f).
+Proof. apply _. Qed.
-- 
GitLab