maxint, minint

Feb 5, 2013 at 3:15 AM
Does Dafny have these? They'd satisfy (forall x:: x<=maxint) etc. Useful for assertions about extrema over possibly empty structures.
Coordinator
Feb 5, 2013 at 3:26 AM
No, not only does Dafny not have notation for "maxint" and "minint", but Dafny does not have a maximum or minimum integer. Integers are unbounded.