Add some _1, _2 lemmas for map_filter
As discussed with @robbertkrebbers
Merge request reports
Activity
assigned to @msammler
unassigned @msammler
- Resolved by Ralf Jung
- Resolved by Ralf Jung
I think the
not_elem_of_dom
andlookup_union_None
lemmas are no-brainers and could be added asap.The filter lemmas are a bit more of a headache since we need to make sure they are consistent with those for set/list.
Could you maybe split up the MR?
Edited by Robbert Krebbers
added 30 commits
-
861b0283...b99e79cf - 29 commits from branch
master
- 8a4b52b7 - Add some _1, _2 lemmas
-
861b0283...b99e79cf - 29 commits from branch
mentioned in merge request !405 (merged)
Status: needs figuring out the names for the new lemmas and making sure they are consistent with sets and lists. @robbertkrebbers says he has some half-finished work somewhere he'll try to dig out.
added S-waiting-for-review label
- Resolved by Michael Sammler
removed S-waiting-for-review label
added S-waiting-for-author label
mentioned in merge request !582 (merged)
added 537 commits
-
18c543b3...d6ba38c3 - 536 commits from branch
master
- a825d7aa - Add some _1, _2 lemmas
-
18c543b3...d6ba38c3 - 536 commits from branch
added 123 commits
-
a825d7aa...e3a6f3ef - 122 commits from branch
master
- df5ac4a9 - Add some _1, _2 lemmas
-
a825d7aa...e3a6f3ef - 122 commits from branch
removed S-waiting-for-author label