ensures + fstar! produces code with out instead of user chosen name

[W95Psp]

trait X {
    fn f() -> u8;
}

#[hax_lib::attributes]
impl X for u8 {
    #[hax_lib::ensures(|result| result == {fstar!("$result")})]
    fn f() -> u8 {
        4
    }
}

Open this code snippet in the playground

Here we get (in F*) the post condition "fun out -> out == result", i.e. the second result doesn't get rewritten.

Workarounds:

• as @mamonet suggested, just always use out in those context
• add a let binding

[W95Psp]

Seems like #872 fixed this issue as well! Using latest hax on the playground shared above produce the expected code!