Dafny 无效标识

【问题标题】：Dafny invalid IdentDafny 无效标识
【发布时间】：2021-07-02 13:16:27
【问题描述】：

我在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。

【问题讨论】：

标签： syntax predicate dafny quantifiers

【解决方案1】：

现在is好像是Dafny中的关键字，所以不能用作变量名。

【讨论】：

非常感谢！我将is 更改为iss，它可以工作。顺便说一句，我回答你（将删除这个）我找不到错误：stackoverflow.com/questions/66563130/…
啊，是的，对不起，我一直没有回复你。我刚刚在那边发帖。