diff options
| -rw-r--r-- | src/Util/Tuple.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 763765898..cf3ce377e 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -780,11 +780,11 @@ 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) +Fixpoint nth_default {A m} (d:A) n : tuple A m -> A := + match m, n with + | O, _ => fun _ => d + | S m', O => hd + | S m', S n' => fun x => nth_default d n' (tl x) end. (* map operation that carries state *) |