愚蠢的无效标识

Question

我在forall行(从is到第一个i(中收到一个invalid Ident错误，有人知道为什么吗？这是不寻常的。

predicate SumMaxToRight(v:array<int>,i:int,s:int)
reads v
requires 0<=i<v.Length
{forall l, is {:induction l} :: 0<=l<=i && is==i+1 ==> Sum(v,l,is)<=s}

版本3.0.0。

Answer 1

看起来is现在是Dafny中的一个关键字，所以它不能用作变量名。