diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-09 12:04:03 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-09 12:04:03 -0500 |
| commit | 02c9f01efc9c4c0316b4fe8c85e3fec3a6c12979 (patch) | |
| tree | 92237e95c4afb3cc7e1237a80dc6081378db621e /src/Util/Tuple.v | |
| parent | 8fa21b4f8e26e9eae1f1fd9061679c57f8603bc1 (diff) | |
Fix Tuple.map2_S
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index d2c3f6d7d..ebfd215a8 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -169,7 +169,7 @@ Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B) - : map2 (n:=S (S n)) f (xs, x) (ys y) = (map2 (n:=S n) f xs ys, f x y). + : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y). Proof. Admitted. |