Draft: Staging MR for various refactorings
It turns out that properly fixing !507 (closed) opened quite a can of worms. We have the following related MRs now:
-
!526 (merged) -
!530 -
!531 (merged) -
non_emptychange as discussed in !526 (comment 97794) -
Direction of equality in fmap/omap/alterlemmas, see !531 (comment 97789)
The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.
Edited by Robbert Krebbers