Search code examples
syntaxpredicatedafnyquantifiers

Dafny invalid Ident

I am getting an invalid Ident error in the forall line (from is to the first i), does anybody know why? This is unusual.

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}

Version 3.0.0.

Solution

  • It looks like is is a keyword in Dafny now, so it cannot be used as a variable name.