From 920dbb90413ecf64424799e2eec15dbc02d1dbfb Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 28 Apr 2017 12:58:21 -0400 Subject: add nth_default on tuple --- src/Util/Tuple.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/Tuple.v') 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) -- cgit v1.2.3