Comprehensions support in Dafny

Oct 6, 2013 at 3:58 PM
Edited Oct 7, 2013 at 2:02 AM
Does Dafny support comprehensions like min, max, sum, count, etc.
Please have a look at this http://research.microsoft.com/en-us/um/people/leino/papers/rmkrml183.pdf
spec# seems to have support for these comprehensions.
Developer
Oct 28, 2013 at 8:25 AM
Hi,

as far as I know Dafny supports set comprehensions (see Test/dafny0/Comprehensions.dfy in the source tree), but, unlike Spec#, it does not directly support min, max, sum, etc..

Best regards,

Valentin