search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.87k stars 256 forks source link

opaque types with members #866

Open erniecohen opened 3 years ago

erniecohen commented 3 years ago

3.0 allows opaque types with members, but trying to use them produces boogie errors. If the implementation was completed so that these could be used and refined (e.g. with datatypes), I would make heavy use of them immediately.

RustanLeino commented 3 years ago

Do you have examples of Boogie errors that were not addressed in PR https://github.com/dafny-lang/dafny/pull/862?

Thanks for your feedback. Updating the refinement features had not been a priority.

RustanLeino commented 3 years ago

It would be great to have an example repro. We will revisit this issue after issues https://github.com/dafny-lang/dafny/issues/864 and https://github.com/dafny-lang/dafny/issues/857 have been fixed.

erniecohen commented 3 years ago

Do you have examples of Boogie errors that were not addressed in PR #862?

No, my bad. I had thought you had filed an issue, but looked and didn't find it, so I thought I should file one just in case.