search

dafny-lang / dafny

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

Remove usage of opaque from standard library #5781

Open keyboardDrummer opened 2 months ago

keyboardDrummer commented 2 months ago

Description

How has this been tested?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

MikaelMayer commented 1 month ago

I would expect to remove this attribute only when the new resolver works on all the existing Dafny files in our codebase, is that your plan too?

keyboardDrummer commented 3 weeks ago

I would expect to remove this attribute only when the new resolver works on all the existing Dafny files in our codebase, is that your plan too?

Hide works using the old resolver as well now, so I think this point is no longer relevant.