From 3df7fe120c0ccbfdb9d4be8d533ff0bfdf2854e3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Apr 2015 16:45:07 -0700
Subject: [PATCH] feat(library/algebra/function): define curry and uncurry
 functions

---
 library/algebra/function.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 3d1b8664ea..980a932b3e 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -42,6 +42,18 @@ definition flip [reducible] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C
 definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
+definition curry [reducible] : (A × B → C) → A → B → C :=
+λ f a b, f (a, b)
+
+definition uncurry [reducible] : (A → B → C) → (A × B → C) :=
+λ f p, match p with (a, b) := f a b end
+
+theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f :=
+rfl
+
+theorem uncurry_curry (f : A × B → C) : uncurry (curry f) = f :=
+funext (λ p, match p with (a, b) := rfl end)
+
 precedence `∘'`:60
 precedence `on`:1
 precedence `$`:1