-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add built-in Map Keys to Seq function #424
Comments
It would be much more natural to expose the keys as a |
Note this is possible within Dafny source, if you use a datatype for which Dafny understands that
Although it may be useful to have a built-in function for performance reasons, I'd love it if this could be part of the standard library, assuming there was a way to generalize over a type |
Note: If the syntax changes, we should also revisit the syntax for seq to multi-set. |
Maps should have a built-in function that outputs its keys in a sequence, given a way to deterministically decide ordering on input.
The text was updated successfully, but these errors were encountered: