Recursion and loops

Suppose we want to compute the nth triangular number:

triangle(n) = 0 + 1 + 2 + ... + (n - 1) + n

We can express this as a simple recursive funciton:

spec fn triangle(n: nat) -> nat
    decreases n,
{
    if n == 0 {
        0
    } else {
        n + triangle((n - 1) as nat)
    }
}

This chapter discusses how to define and use recursive functions, including writing decreases clauses and using fuel. It then explores a series of verified implementations of triangle, starting with a basic recursive implementation and ending with a while loop.