diff options
Diffstat (limited to 'src/Util/Tuple.v')
-rw-r--r-- | src/Util/Tuple.v | 15 |
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 := |