We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 511511c commit f24b343Copy full SHA for f24b343
theories/Lists/List.v
@@ -3577,7 +3577,7 @@ Global Hint Rewrite
3577
rev_involutive (* rev (rev l) = l *)
3578
rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
3579
map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
3580
- length_app (* length (map f l) = length l *)
+ length_map (* length (map f l) = length l *)
3581
length_seq (* length (seq start len) = len *)
3582
length_app (* length (l ++ l') = length l + length l' *)
3583
length_rev (* length (rev l) = length l *)
0 commit comments