Attribute Macro decreases

#[decreases]

Provide a measure for a function: this measure will be used once extracted in a backend for checking termination. The expression that decreases can be of any type. (TODO: this is probably as it is true only for F*, see #297)

Example

use hax_lib_macros::*;
#[decreases((m, n))]
pub fn ackermann(m: u64, n: u64) -> u64 {
    match (m, n) {
        (0, _) => n + 1,
        (_, 0) => ackermann(m - 1, 1),
        _ => ackermann(m - 1, ackermann(m, n - 1)),
    }
}