Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Maps: add MapKeys, MapValues, and related helpers #86

Open
wants to merge 14 commits into
base: master
Choose a base branch
from

Conversation

alex-chew
Copy link
Contributor

This PR addresses a common use case where one wants to map an injective function over the keys of the map, retaining the values.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

davidcok
davidcok previously approved these changes Feb 13, 2023
@alex-chew alex-chew enabled auto-merge (squash) February 13, 2023 22:29
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor typo, otherwise looks good!

src/Collections/Maps/Maps.dfy Outdated Show resolved Hide resolved
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
src/Collections/Maps/Maps.dfy Show resolved Hide resolved
src/Collections/Maps/Maps.dfy Show resolved Hide resolved
src/Collections/Maps/Maps.dfy Show resolved Hide resolved
@alex-chew alex-chew changed the title Maps: add MapKeys Maps: add MapKeys, MapValues, and related helpers Apr 19, 2023
robin-aws
robin-aws previously approved these changes Apr 19, 2023
Copy link
Member

@robin-aws robin-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, made some non-blocking suggestions (because we have the opportunity to improve naming before this code is more locked down)

src/Collections/Maps/Maps.dfy Outdated Show resolved Hide resolved
src/Collections/Maps/Maps.dfy Outdated Show resolved Hide resolved
@robin-aws
Copy link
Member

See also: #119. I don't want to block on adding this under src/dafny as well but do want to track that work.

@alex-chew
Copy link
Contributor Author

See also: #119. I don't want to block on adding this under src/dafny as well but do want to track that work.

I'll take care of syncing to src/dafny as a follow-up, once this PR is finalized.

@alex-chew alex-chew requested a review from robin-aws April 19, 2023 21:28
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants