From dfb7398c3d674ef9762b6d9a9d47029a8d66167c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 17:58:03 -0400 Subject: Add Tuple.eta --- src/Util/Tuple.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/Util/Tuple.v') 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 := -- cgit v1.2.3