Skip to content
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

Implement sequence comprehensions #2335

Open
robin-aws opened this issue Jun 30, 2022 · 1 comment
Open

Implement sequence comprehensions #2335

robin-aws opened this issue Jun 30, 2022 · 1 comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself

Comments

@robin-aws
Copy link
Member

robin-aws commented Jun 30, 2022

As proposed in dafny-lang/rfcs#10

@robin-aws robin-aws added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself labels Jun 30, 2022
@kjx
Copy link

kjx commented Oct 14, 2022

yes please!

and either some way of enumerating (multi)sets, or at least an "ordered set" in a library?

this is not sorted - because ordering is on insertion order/position (like a seq) not element comparisons.
or you can think of it as a seq where equality is defined over the set of elements.

I've pretty much built one, but it's not at all pretty --- it's parallel primitive set, seq, and map, and assumes
elements have equality (which they MUST to go in a set in the first place, right?). I guess one could just
use set comprehensions on the seqs but keeping them parallel seems to work a little better.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: language definition Relating to the Dafny language definition itself
Projects
None yet
Development

No branches or pull requests

2 participants