Iteration over a range of "negative" length in F*

[maximebuyse]

fn find (v: &mut Vec<u8>, x: u8) -> bool {
    let mut res = false;
    for i in 1..v.len() {
        if v[i] == x {
            res = true
        }
    }
    res
}

Open this code snippet in the playground

In the example above, F* type-checking fails saying that v[i] cannot be proven to be an access in bounds. If the range of the loop is 0..v.len() it can be proven.

This seems to be a problem with Rust_primitives.Hax.Folds.fold_range when the beginning of the range is possibly strictly inferior to the end of the range.