Several simple lemmas.

Thanks for the MR! Robbert is currently on vacation (for two more weeks I think), when he's back he will look at this.

Thank you very much for the MR. I left a bunch of comments.

added 1 commit

• 750d8f52 - Implement suggestions by Robbert Krebbers on fin_maps’ lemmas.

Compare with previous version

added 1 commit

• 88fa9552 - Implement suggestions by Robbert Krebbers on gmap.

Compare with previous version

added 1 commit

• 0c6f8fb1 - Implement suggestions by Robbert Krebbers on list’s lemmas.

Compare with previous version

added 1 commit

• 512d7073 - Additional changes in list's lemmas.

Compare with previous version

added 1 commit

• 369f793b - Remove 'NoDup' lemma.

Compare with previous version

LGTM. Could you squash the comments and add a commit in which you add yourself as a contributor for stdpp 1.2.1 in CHANGELOG.md?

Maybe also change "A bunch of new lemmas for list operations" into "A bunch of new lemmas for list, set, and map operations."

I did just that.

Thanks for including me as a contributor for this next release. Also, thanks for all the detailed instructions on the previous comments.

Thank you very much too!

I see there is still a merge commit in the MR. So somehow the rebase didn't fully work?

My fault.

resolved all threads

added 2 commits

• f067cd18 - Add new lemmas for list, set, and map operations.
• 44d3e6e4 - Merge remote-tracking branch 'origin'

Compare with previous version

added 7 commits

• f067cd18...f9830af6 - 5 commits from branch iris:master
• ea126d8e - Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp
• 146e35f0 - Update CHANGELOG.md

Compare with previous version

added 1 commit

• 6bc8803a - Add new lemmas for list, set, and map operations.

Compare with previous version

merged

mentioned in commit 48067dec

Merged, thank you very much for the MR!