diff options
author | Jason Gross <jgross@mit.edu> | 2018-05-21 20:10:36 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-05-21 23:08:58 -0400 |
commit | 60c83608df9ef701ad559381288931dd61749f38 (patch) | |
tree | 1c23087942417412b87ec60dcedf301f6044d935 | |
parent | 8ac227a2e1b13ee5a24fd6a892208996338476c3 (diff) |
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.
-rw-r--r-- | src/Util/ListUtil.v | 22 |
1 files changed, 13 insertions, 9 deletions
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} := |