Dafny 4.0 suggestion: for i <- 0 to 10 instead of for i := 0 to 10

[MikaelMayer]

Currently, to write a for loop, we use

for i := 0 to 10 {
}

Since the introduction of sequences, it would be nicer to be able to write

for i <- 0 to 10 {
}

or simply more unambiguously

for i | 0 <= i < 10 {
}

[robin-aws]

for i <- 0 to 10 {
}

I definitely like this, since it would be consistent with the follow-up idea we had from the ordered quantification RFC of supporting the same thing in foreach loops and sequence comprehensions (e.g. seq i <- 0 to 10 :: i * i).

It does mean that foreach i <- 0 to 10 { } would mean exactly the same thing though, so unless having for as a separate, more limited form makes verification MUCH easier (unlikely since we could keep the current encoding as a special case), I'd be inclined to deprecate and drop for at that point.

So my preference would be to add support for lo to hi as a quantifier variable domain (possibly by supporting it as independent syntax for sequence values). I've cut that as a separate issue: #2583

for i | 0 <= i < 10 {
}

This we shouldn't do, since you only have a well-defined ordering for quantification if you declare a domain for the variable (i.e. i <- <C>). For an arbitrary type T, there isn't an obvious way to order values that match for t: T | P(t) {}.

[MikaelMayer]

I'm in for keeping only the first one then.

[davidcok]

Use .. instead of 'to

[robin-aws]

Will also discuss the larger possibility of replacing for with foreach (which needs significant discussion)