From 8344ce425aebc86e41b8b333a3afaa06ba42af29 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Sep 2017 00:39:17 +0200
Subject: [PATCH] Add uncurry3 and uncurry4.

---
 theories/base.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index fb129db3..1a147388 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -482,6 +482,11 @@ Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
 Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
   let '(a,b,c,d) := p in f a b c d.
 
+Definition uncurry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
+  f (a, b, c).
+Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
+  (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).
+
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
 Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
-- 
GitLab