Skip to content

Commit d1933c9

Browse files
remove length_app_comm from rewrite hint database
1 parent 2877d15 commit d1933c9

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

theories/Lists/List.v

-1
Original file line numberDiff line numberDiff line change
@@ -3980,7 +3980,6 @@ Global Hint Rewrite
39803980
length_map (* length (map f l) = length l *)
39813981
length_seq (* length (seq start len) = len *)
39823982
length_app (* length (l ++ l') = length l + length l' *)
3983-
length_app_comm (* length (l ++ l') = length (l' ++ l) *)
39843983
length_rev (* length (rev l) = length l *)
39853984
app_nil_r (* l ++ nil = l *)
39863985
: list.

0 commit comments

Comments
 (0)