[Lean] Arrays with non-integer-literal size

[clementblaudeau]

Currently, the Lean Backend only supports arrays where the size is an integer literal. This was done to avoid issues of type equality between types like Vector Nat 5 and Vector Nat (5:usize).toNat. Instead, a proper treatment of usize should help lifting this restriction, having any pure expression as a vector size.

[clementblaudeau]

It should be possible to have do-blocks in array-length expressions. Returns are forbidden (see https://doc.rust-lang.org/stable/error_codes/E0572.html)