At the very least the Valid()/Repr idiom is not something Dafny users tend to stumble on by themselves. That idiom is also very general, and a more structured specialization of it would be good enough for a lot of Dafny code and much easier to work with.
22 is a very basic first step towards this but unfortunately blocked by https://github.com/dafny-lang/dafny/issues/1588. It may be possible to avoid that and @seebees and @jtristan have been working on an alternative.
At the very least the
Valid()/Repridiom is not something Dafny users tend to stumble on by themselves. That idiom is also very general, and a more structured specialization of it would be good enough for a lot of Dafny code and much easier to work with.22 is a very basic first step towards this but unfortunately blocked by https://github.com/dafny-lang/dafny/issues/1588. It may be possible to avoid that and @seebees and @jtristan have been working on an alternative.