Attribute Macro lemma

#[lemma]

Mark a Proof<{STATEMENT}>-returning function as a lemma, where STATEMENT is a Prop expression capturing any input variable. In the backends, this will generate a lemma with an empty proof.

Example

use hax_lib_macros::*;
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)),
    }
}

#[lemma]
/// $`\forall n \in \mathbb{N}, \textrm{ackermann}(2, n) = 2 (n + 3) - 3`$
pub fn ackermann_property_m1(n: u64) -> Proof<{ ackermann(2, n) == 2 * (n + 3) - 3 }> {}