diff options
author | jadep <jade.philipoom@gmail.com> | 2017-04-28 12:58:21 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2017-04-28 12:58:21 -0400 |
commit | 920dbb90413ecf64424799e2eec15dbc02d1dbfb (patch) | |
tree | d29b19f3771a169cb37f82d3ad7bc639fbee23b6 | |
parent | 01a6557cd14bab453f09ec4448682f05bdb607f6 (diff) |
add nth_default on tuple
-rw-r--r-- | src/Util/Tuple.v | 7 |
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) |