Macro loop_decreases

loop_decreases!() { /* proc-macro */ }

Must be used to prove termination of while loops. This takes an expression that should be a usize that decreases at every iteration

This function must be called just after loop_invariant, or at the first line of the loop if there is no invariant.