It would be tricky for type inference to decide if you want all of int or just the subrange
nat . The difference plays a role exactly in quantifications, as you have found. For example, what would you say should be the type of
x in:
forall x :: if P(x) then 1000 <= Fact(x) else 0 <= x
where
predicate P(y: int)
{
100 <= y
}
function Fact(n: nat): nat
{
... // as above
}
If x is inferred as int , the value of the forall expression is
false , whereas if x is inferred as the subrange nat , then the
forall expression would be true .
Here's an even simpler example:
forall x :: 0 <= x
What should be the type of x , int or nat ?
It is for this reason that Dafny does not infer types of quantified variables to be subrange types.
If you wonder about what type has been inferred for a variable, just hover over the name of the variable in the Dafny IDE in Visual Studio and the hover text will tell you.
Rustan
