diff options
-rw-r--r-- | src/Util/Tuple.v | 18 |
1 files changed, 18 insertions, 0 deletions
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 |