add nth_default on tuple

1 files changed, 7 insertions, 0 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 615410f2a..763765898 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -780,6 +780,13 @@ Lemma map_append {A B n} (f:A->B) : forall (x:tuple A n) (a:A),
   map f (append a x) = append (f a) (map f x).
 Proof. destruct n; auto using map_append'. Qed.
 
+Fixpoint nth_default {A m} (d:A) n (x: tuple A m) : A :=
+  match m,n with
+  | O, _ => d
+  | S m', O => hd x
+  | S m', S n' => nth_default d n' (tl x)
+  end.
+
 (* map operation that carries state *)
 (* first argument to f is index in tuple *)
 Fixpoint mapi_with' {T A B n} i (f: nat->T->A->T*B) (start:T)