creusot_contracts::macros

Attribute Macro terminates

#[terminates]
Expand description

Indicate that the function terminates: fulfilling the requires clauses ensures that this function will not loop forever.