Macro vec 

macro_rules! vec {
    () => { ... };
    ($elem:expr; $n:expr) => { ... };
    ($($x:expr),*) => { ... };
    ($($x:expr,)*) => { ... };
}

Creusot-friendly replacement of vec!

The std vec macro uses special magic to construct the array argument to Box::new directly on the heap. Because the generated MIR is hard to translate, we provide a custom vec! macro which does not do this.