About repeat expression in array

[zpzigi754]

I've tested with the below example.

#![allow(unused_imports)]
use vstd::prelude::*;

verus! {

fn main() {
    let array: [i32; 3] = [0; 3];
    // XXX: if the below is used, it would work
    //let array: [i32; 3] = [0, 0, 0];
}

} // verus!

It says that The verifier does not yet support the following Rust feature: repeat expressions. I think that supporting the repeat expression in array initialization would be helpful for the users if the size of the target array to verify is big.

Is there any alternative way of creating a large array without the repeat expression in verus?
I also wonder what is the main obstacle of supporting the repeat expression in verus.

[utaal]

Hi @zpzigi754, thanks for the report, and for trying out Verus!
I don't think we currently have a workaround for this, (@tjhance ?).
Anyway, while this is indeed important, it's a feature request -- so I'll convert it to a discussion.

[zpzigi754]

Thank you very much, @utaal and @tjhance. I've confirmed that repeat is now supported for Copy type in the latest main branch.