diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-11 09:17:09 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-11 09:17:09 -0400 |
| commit | a37eb79f7750a419346211abb58ec45b79975da0 (patch) | |
| tree | ba62e0ff6176a8dc208f65bfae52c8415076d107 /src/Util/ListUtil.v | |
| parent | 2e566c32baf2a140cd7820c4f06437ee5c43ac44 (diff) | |
starting rewrite using different definition of map
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 36d8a3ad3..dd1e6a5c5 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -258,13 +258,13 @@ Proof. destruct (lt_dec n (length xs)); auto. Qed. -Lemma combine_truncate_r : forall {A} (xs ys : list A), +Lemma combine_truncate_r : forall {A B} (xs : list A) (ys : list B), combine xs ys = combine xs (firstn (length xs) ys). Proof. induction xs; destruct ys; boring. Qed. -Lemma combine_truncate_l : forall {A} (xs ys : list A), +Lemma combine_truncate_l : forall {A B} (xs : list A) (ys : list B), combine xs ys = combine (firstn (length ys) xs) ys. Proof. induction xs; destruct ys; boring. |