maxint, minint

Feb 5, 2013 at 2: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 2: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.