Skip to content
GitLab
Projects
Groups
Topics
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Register
Sign in
Toggle navigation
Menu
Iris
stdpp
Merge requests
!282
Add lemmas `map_intersection_filter` and `map_difference_filter`.
Code
Review changes
Check out branch
Download
Patches
Plain diff
Merged
Robbert Krebbers
requested to merge
robbert/intersection_difference_filter
into
master
Jun 17, 2021
Overview
2
Commits
1
Pipelines
3
Changes
1
See also the discussion in
iris!697 (diffs, comment 69805)
Edited
Jun 17, 2021
by
Robbert Krebbers