From 60c83608df9ef701ad559381288931dd61749f38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 May 2018 20:10:36 -0400 Subject: Move function argument out of fixpoint of List.map2 This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now. --- src/Util/ListUtil.v | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 92c648725..8cfb626d2 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -107,7 +107,7 @@ Module Export List. End FlatMap. Hint Rewrite @flat_map_cons @flat_map_nil : push_flat_map. - Lemma rev_cons {A} x ls : @rev A (x :: ls) = rev ls ++ [x]. Proof. reflexivity. Qed. + Lemma rev_cons {A} x ls : @rev A (x :: ls) = rev ls ++ [x]. Proof. reflexivity. Qed. Hint Rewrite @rev_cons : list. Section FoldRight. @@ -283,14 +283,18 @@ Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l). Definition sum xs := sum_firstn xs (length xs). -Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C := - match la with - | nil => nil - | a :: la' => match lb with - | nil => nil - | b :: lb' => f a b :: map2 f la' lb' - end - end. +Section map2. + Context {A B C} + (f : A -> B -> C). + + Fixpoint map2 (la : list A) (lb : list B) : list C := + match la, lb with + | nil, _ => nil + | _, nil => nil + | a :: la', b :: lb' + => f a b :: map2 la' lb' + end. +End map2. (* xs[n] := f xs[n] *) Fixpoint update_nth {T} n f (xs:list T) {struct n} := -- cgit v1.2.3