Skip to content

feat: add gmultiset camera#187

Draft
alok wants to merge 4 commits intoleanprover-community:masterfrom
alok:codex/pr-gmultiset
Draft

feat: add gmultiset camera#187
alok wants to merge 4 commits intoleanprover-community:masterfrom
alok:codex/pr-gmultiset

Conversation

@alok
Copy link
Copy Markdown
Contributor

@alok alok commented Mar 20, 2026

Summary

  • add GMultiset.lean as a discrete TreeMap-backed multiset camera
  • enforce strictly positive multiplicities in the carrier so the CMRA laws match multiset semantics
  • add the core update lemmas, including the generic local update
  • export it from Iris.Algebra
  • mark the gmultiset.v CMRA and Updates portions done in PORTING.md

Verification

  • lake build Iris.Algebra.GMultiset Iris.Algebra
  • lake build

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant