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