Add map_agree
As discussed with @robbertkrebbers. I am not sure if there are good lemmas for insert and union of map_agree (i.e. corresponding to map_disjoint_union_l and map_disjoint_insert_l). Do you have ideas for how they would look like?
Merge request reports
Activity
assigned to @msammler
unassigned @msammler
added 7 commits
-
746faf78...224790c8 - 6 commits from branch
master - fd97f033 - Add map_agree
-
746faf78...224790c8 - 6 commits from branch
I am not sure if there are good lemmas for insert and union of
map_agree(i.e. corresponding tomap_disjoint_union_landmap_disjoint_insert_l). Do you have ideas for how they would look like?IF you just replace map_disjoint with map_agree, they appear false. I don't see any reasonable alternatives that make them true. I propose that we just leave them, and if someone comes with an idea, we can always add them later.
- Resolved by Robbert Krebbers
This MR looks good to me.
Can you rebase on !398 (merged) (which is merged into master once CI finishes) and add a CHANGELOG?
- Last reply by Michael Sammler
added 19 commits
-
f9803c7c...6f1ca045 - 17 commits from branch
master - 6b4ebe6e - Add map_agree
- cf3242c0 - Tweak some proofs.
-
f9803c7c...6f1ca045 - 17 commits from branch
added 3 commits
