From e3b69200fae4bc11fa9843b1123884e7aef9d6a8 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 12 Jul 2016 20:41:51 -0400 Subject: tuple: applying functions to tuples of arbitrary length --- src/Util/Tuple.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 13f8bd386..05d47b7f8 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -177,3 +177,21 @@ Proof. induction xs; destruct n; intros; try solve [simpl in *; congruence]. apply from_list_default'_eq. Qed. + +Fixpoint function R T n : Type := + match n with + | O => R + | S n' => T -> function R T n' + end. + +Fixpoint apply' {R T} (n:nat) : (T -> function R T n) -> tuple' T n -> R := + match n with + | 0 => id + | S n' => fun f x => apply' n' (f (snd x)) (fst x) + end. + +Definition apply {R T} (n:nat) : function R T n -> tuple T n -> R := + match n with + | O => fun r _ => r + | S n' => fun f x => apply' n' f x + end. \ No newline at end of file -- cgit v1.2.3