Skip to content
Snippets Groups Projects

Misc lemmas for maps

Merged Misc lemmas for maps
robbert/misc_map into master
Merged Robbert Krebbers requested to merge robbert/misc_map into master
  • Add lemmas merge_empty_l and merge_empty_r.
  • Add lemma map_filter_lookup.
  • Add lemma map_fmap_singleton_inv.

Merge request reports

Merge request pipeline #48710 passed

Stage: build

Merge request pipeline passed for deebe088

Approval is optional

Merged by Robbert KrebbersRobbert Krebbers 3 years ago (Jun 15, 2021 4:49pm UTC)

Loading

Pipeline #48714 passed

Stage: build

Pipeline passed for ed5b8dd4 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply