Struct Postcondition 

pub struct Postcondition {
    pub result_binder: Pat,
    pub body: Expr,
}

A postcondition.

Example

The expression result != x in the following is a postcondition. Note that result is an extra binder that represent the result of f, whose type is u8 in this case: the return type of f.

#[hax_lib::ensures(|result| result != x)]
fn f(x: u8) -> u8 { x.wrapping_add(1) }

Fields

result_binder: Pat

In the example, this is |result|.

body: Expr

The formula of the postcondition, result != x in the example.