Support <lo> to <hi> as a quantifier variable domain, or as a sequence display

[robin-aws]

Another follow-up idea from the change to add the x <- C quantified variable domain syntax: dafny-lang/rfcs#10 (comment)

Because we decided to require a quantified variable domain for ordered quantifications, and therefore seq i | 0 <= i < n :: f(i) | P(i) is not allowed, we still need the often-maligned seq(n, f) "sequence construction" syntax: #1332.

One way to replace the old syntax is to support range expressions like 0 to 5 as at least quantified variable domains, or (my preference) as fully independent syntax for a sequence value. The runtime representation would be a distinct RangeSequence<T> case, rather than explicitly allocating the range of values. This would be relatively cheap to implement once the sequence type has a single implementation in Dafny source code rather than N implementations in each runtime (after #2390).

(marking this as a breaking change not only because deprecated and removing sequence constructions would be breaking, but also in case the parsing change turns out to be breaking - I've been burnt before :)

[davidcok]

Why not use i <- 0 .. 10 ?

[MikaelMayer]

Why not use i <- 0 .. 10 ?

Why not indeed, since it's consistent with sequence extraction.

[robin-aws]

I experimented with a parser change to support this and it did not break any existing test cases, so I'm comfortable removing the breaking-change label.