Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming
!507 (closed) ballooned into this huge change. This contains the following two MRs:
There is more that could be done, but that is postponed (we should probably open an issue):
-
non_empty
change as discussed in !526 (comment 97794) -
Direction of equality in fmap
/omap
/alter
lemmas, see !531 (comment 97789)
Merge request reports
Activity
mentioned in merge request !526 (merged)
mentioned in merge request !530 (merged)
added 6 commits
Toggle commit listmentioned in merge request !531 (merged)
mentioned in issue #196
added 7 commits
- d9a6e55e - Make `lookup` and `elem_of` lemmas for `list` consistent with those for map and set.
- 44d3349c - CHANGELOG.
- 9d2e6d60 - Also fix `elem_of_list` → `list_elem_of` inconsistency.
- d624ecd7 - Rename `list_alter_fmap` → `list_fmap_alter`, remove `list_alter_fmap_mono`.
- facb9097 - Fix bug in CHANGELOG.
- 07c4f0ee - Rename `list_elem_of_fmap_2_alt` → `list_elem_of_fmap_2'`.
- 1d28e9c0 - Merge branch 'robbert/list_fmap_lemmas' into 'ci/refactor_staging'
Toggle commit listmarked the checklist item !531 (merged) as completed
@robbertkrebbers what is the status of this? We have some already approved MRs sitting here and waiting; if we don't know when the rest of these changes will land then maybe it doesn't make sense to stage them all together?
The plan for this one is that the two MRs merged into this should still be landed but we don't try to include further changes into this. So it needs a rebase with its current contents, possibly adjustment for !530 (merged), and then should go ahead.
But !439 takes priority.
Edited by Ralf Jungadded S-waiting-for-author label