Attribute Macro creusot_contracts::macros::terminates
#[terminates]
Expand description
Indicate that the function terminates: fulfilling the requires
clauses
ensures that this function will not loop forever.
#[terminates]
Indicate that the function terminates: fulfilling the requires
clauses
ensures that this function will not loop forever.