Dafny for-loop с оператором forall?

Я некоторое время работал в Dafny, и если мне приходилось использовать цикл for, я использовал оператор while, потому что я думал, что цикл for не существует в Dafny как встроенный.

Однако по этой ссылке (Dafny, триггеры в назначении forall) я увидел, что код использует оператор forall как for:

    method toArrayConvert(s:seq<int>) returns(res:array<int>)
    requires |s|>0;
    ensures |s| == res.Length;
    ensures forall i::0<=i<res.Length ==> s[i] == res[i];
    {
      res :=new int[|s|];
      forall i|0<=i && i<|s| {res[i]:=s[i];}  /*on this line I get the following*/
     // rewrite: forall i#inv: int {:trigger res[i#inv]} | 0 <= i#inv && i#inv < |s| { res[i#inv] := s[i#inv]; }
    //Not generating triggers for "res[i#inv] == s[i#inv]".
      return res;
    }

Я думал, что forall используется только как квантификатор в точках проверки (утверждения, постусловия, инварианты...) и недействителен для циклов. Я что-то неправильно понимаю?

PS:

Также по той же ссылке у меня есть еще один вопрос. Когда я заменяю строку с ошибкой:

forall i|0<=i && i<|s| {res[i]:=s[i];}

by

forall i: int {:trigger res[i]} | 0 <= i && i < |s| { res[i] := s[i]; }

Как это видно по коду:

  method toArrayConvert(s:seq<int>) returns(res:array<int>)
    requires |s|>0;
    ensures |s| == res.Length;
    ensures forall i::0<=i<res.Length ==> s[i] == res[i];
    {
      res :=new int[|s|];
      //forall i|0<=i && i<|s| {res[i]:=s[i];}  /*on this line I get the following*/
      forall i: int {:trigger res[i]} | 0 <= i && i < |s| { res[i] := s[i]; }
    //Not generating triggers for "res[i#inv] == s[i#inv]".
      return res;
    }

Выдает ошибку: unresolved identifier: i

Что здесь происходит? Нужно ли использовать что-то вроде i#inv вместо i, как говорит отладчик? Но это также дает мне ошибки.