[Lean] Turn the rejection phase into a transformation phase

[clementblaudeau]

[maximebuyse]

Example of code producing this error (and workaround for this specific case):

fn f(x: Option<usize>) -> Option<usize> {
    1usize.checked_add(match x {
        Some(n) => n,
        _ => 0
    })
}

fn f_working(x: Option<usize>) -> Option<usize> {
    1usize.checked_add(x.unwrap_or(0))
}

Open this code snippet in the playground

[abentkamp]

#1840 was supposed to fix this, but unfortunately it doesn't.

pub enum Ordering {
    Less = -1,
    Equal = 0,
    Greater = 1,
}
fn partial_cmp(x: u8, y: u8) -> Option<Ordering> {
    Option::Some(if x < y {Ordering::Less}
    else if x > y {Ordering::Greater}
    else {Ordering::Equal})
}

Hax Playground

Lean says:

error: Playground.lean:45:10: invalid use of `(<- ...)`, must be nested inside a 'do' expression

@rusch95 Feel free to look into this if you like.

[rusch95]

Will do

[abentkamp]

Once this is resolved, we should delete the rejection phase.

[abentkamp]

@rusch95 It turns out that the remaining issue above was fairly independent of what you did. #1954 should fix it.