Attribute Macro variant 

#[variant]

Declares a variant for a function or a loop.

This is primarily used in combination with recursive logical functions.

The variant must be an expression whose type implements WellFounded.

Example

• Recursive logical function:

#[logic]
#[variant(x)]
#[requires(x >= 0)]
fn recursive_add(x: Int, y: Int) -> Int {
    if x == 0 {
        y
    } else {
        recursive_add(x - 1, y + 1)
    }
}

• Loop variant:

#[check(terminates)]
#[ensures(result == x)]
fn inneficient_identity(mut x: i32) -> i32 {
    let mut res = 0;
    let total = snapshot!(x);
    // Attribute on loop are experimental in Rust, just pretend the next 2 lines are uncommented :)
    // #[variant(x)]
    // #[invariant(x@ + res@ == total@)]
    while x > 0 {
        x -= 1;
        res += 1;
    }
    res
}