For Loops #

The previous section introduced a while loop implementation of triangle:

{{#include ../../../../examples/guide/recursion.rs:loop}}

We can rewrite this as a for loop as follows:

{{#include ../../../../examples/guide/recursion.rs:for_loop}}

The only difference between this for loop and the while loop is that idx is automatically incremented by 1 at the end of each iteration, and we no longer need the idx <= n invariant.

For more complex examples, Verus also provides ghost specifications about the iterator used in for loops, as we discuss in the next section.