Attribute Macro creusot_contracts::macros::variant

#[variant]
Expand description

Declares a variant for a function

This is primarily used in combination with recursive logical functions.

The variant must be an expression which returns a type implementing WellFounded.

§Example

#[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)
    }
}