And it doesn't have global variables that you could lift to? I ask mostly because I don't have a great answer for the other question. (The answer should be “oh, you can specify types that a variable can't be, and just use that when you make a decision that precludes certain types without having to fully commit to a type”, as we've discussed, but I still haven't implemented that.) On Fri, Aug 27, 2021 at 04:03:30PM -0700, Sorawee Porncharoenwase wrote:
Oh, and about this question:In Dafny do function expressions not generate closures?It does, but an important part of the language is top-level function expression definition, which would not have a lifting target. So yes, choice-filters-to-apply seems like a solution, but see my above question about how to use it properly. Thanks!