Add for loop for Verus Documentation

source/docs/guide/src/SUMMARY.md

@@ -24,6 +24,7 @@
     - [Recursive exec and proof functions, proofs by induction](induction.md)
     - [Loops and invariants](while.md)
         - [Loops with break](break.md)
+        - [For Loops](for.md)
     - [Lexicographic decreases clauses and mutual recursion](lex_mutual.md)
 - [Datatypes: struct and enum]() <!--- Andrea --->
     - [Defining datatypes]() <!--- Andrea --->

source/docs/guide/src/for.md

@@ -0,0 +1,22 @@
+# For Loops 
+
+The previous section introduced a `while` loop implementation of `triangle`:
+
+```rust
+{{#include ../../../rust_verify/example/guide/recursion.rs:loop}}
+```
+
+We can rewrite this as a `for` loop as follows:
+
+```rust
+{{#include ../../../rust_verify/example/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 the 
+each iteration. 
+
+In addition, `iter.start`, `iter.cur`, `iter.end` reveal the start, current, and end
+for the iterator of range `0..n`. 
+`iter@` records all the elements that the iterator has iterated so far. 
+In the above example, if `idx=3`, `iter@ =~= seq![0,1,2]`

source/rust_verify/example/guide/recursion.rs

@@ -275,6 +275,30 @@ fn loop_triangle_break(n: u32) -> (sum: u32)
 }
 // ANCHOR_END: loop_break
 
+// ANCHOR: for_loop
+fn for_loop_triangle(n: u32) -> (sum: u32)
+    requires
+        triangle(n as nat) < 0x1_0000_0000,
+    ensures
+        sum == triangle(n as nat),
+{
+    let mut sum: u32 = 0;
+
+    for idx in iter: 0..n
+        invariant
+            sum == triangle(idx as nat),
+            triangle(n as nat) < 0x1_0000_0000,
+    {
+        assert(sum + idx + 1 < 0x1_0000_0000) by {
+            triangle_is_monotonic((idx + 1) as nat, n as nat);
+        }
+        sum = sum + idx + 1;
+    }
+    sum
+}
+// ANCHOR_END: for_loop
+
+
 // ANCHOR: ackermann
 spec fn ackermann(m: nat, n: nat) -> nat
     decreases m, n,