История изменений
Исправление tailgunner, (текущая версия) :
Представим что вот этого куса кода и нет. Вопрос: будет ли ругаться анализатор и на что.
Если анализатор проверяет выходы за границу цикла - да, он должен ругаться.
Это к вопросу что не получатся ли в итоге зависимые типы («idx зависит от arr»).
Брать информацию из предусловия или определения типа - разница не принципиальная.
Исходная версия tailgunner, :
Представим что вот этого куса кода и нет. Вопрос: будет ли ругаться анализатор и на что.
Если анализатор проверяет выходы за границу цикла - да, он должен ругаться.
Это к вопросу что не получатся ли в итоге зависимые типы («idx зависит от arr»).
Брать информацию из предусловия или определения типа - разниуа не принципиальная.