This is an early draft of a design for an Enumerable<T> trait, which I developed in the process of writing up an RFC for adding some kind of enumeration support to Dafny: https://github.com/dafny-lang/dafny/issues/1753
I do NOT expect this to be approved even once it is more polished, since it has the same issue with needing the {:termination false} attribute that my other PR (#22) is blocked by. I will likely tackle at least a partial solution to that issue (https://github.com/dafny-lang/dafny/issues/1588) before promoting this PR out of draft. I nevertheless wanted to create this PR for early feedback and as evidence that all the common enumeration use cases therein do in fact verify, and therefore to support the arguments in the RFC I'll be posting to dafny-lang/rfcs shortly.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
This is an early draft of a design for an
Enumerable<T>trait, which I developed in the process of writing up an RFC for adding some kind of enumeration support to Dafny: https://github.com/dafny-lang/dafny/issues/1753I do NOT expect this to be approved even once it is more polished, since it has the same issue with needing the
{:termination false}attribute that my other PR (#22) is blocked by. I will likely tackle at least a partial solution to that issue (https://github.com/dafny-lang/dafny/issues/1588) before promoting this PR out of draft. I nevertheless wanted to create this PR for early feedback and as evidence that all the common enumeration use cases therein do in fact verify, and therefore to support the arguments in the RFC I'll be posting todafny-lang/rfcsshortly.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.