Robin Salkeld

More specifically (since the lack of `:| expect` came up in https://github.com/dafny-lang/dafny/issues/5165), I'd suggest both of these options: ``` var y :| expect P(y); // Only allowed if the domain...

https://github.com/dafny-lang/dafny/pull/5342 was reverted so I'm reopening this in case we want to revisit. Also adding a somewhat-related observation: if you are trying to fix a nightly build break in a...

> Lots of things LOL Is making verification consistent in scope?

This is a good thing to be concerned about in general. For the record some language ecosystems deal with this program at a higher-level of tooling instead. For example, `.jar`...

Note the solution to the translation integrity version of the problem can probably leverage the `.dtr` translation record concept we proposed on #5140 as well - if those files also...

Hi @txiang61! Yes, this is something we're actively trying to design for now, and we'll communicate more on the solution as we converge. You might want to have a look...