Add Tuple.eta

1 files changed, 15 insertions, 0 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index cdae79191..2b049d86e 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -208,6 +208,21 @@ Fixpoint curry {R T n} : curryT R T n -> (tuple T n -> R)
      | S n' => @curry' R T n'
      end.
 
+Fixpoint eta' {n A B} : (tuple' A n -> B) -> tuple' A n -> B
+  := match n with
+     | 0 => fun f => f
+     | S n' => fun (f : tuple' A n' * A -> B)
+                   (xy : tuple' A n' * A)
+               => let '(x, y) := xy in
+                  eta' (fun x => f (x, y)) x
+     end.
+
+Definition eta {n A B} : (tuple A n -> B) -> tuple A n -> B
+  := match n with
+     | 0 => fun f => f
+     | S n' => @eta' n' A B
+     end.
+
 Definition on_tuple {A B} (f:list A -> list B)
            {n m:nat} (H:forall xs, length xs = n -> length (f xs) = m)
            (xs:tuple A n) : tuple B m :=