Commit 2022-09-06 02:53 58903102
View on Github →feat(src/data/*): lemmas about emptiness for finset/multiset/vector coercions (#16113)
Adds basic lemmas about whether the result of to_list
is empty for various data structures.
feat(src/data/*): lemmas about emptiness for finset/multiset/vector coercions (#16113)
Adds basic lemmas about whether the result of to_list
is empty for various data structures.