search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Support `from_fn` for two-dimensional arrays. #39

Open karthikbhargavan opened 2 months ago

karthikbhargavan commented 2 months ago

The following code does not work in Eurydice:

let A = core::array::from_fn(|i| {
            core::array::from_fn(|j| A_transpose[j][i])
    });
msprotz commented 2 months ago

The minimized repro is here: https://github.com/AeneasVerif/eurydice/blob/main/test/closure/src/main.rs

msprotz commented 2 months ago

(test currently disabled because it is, rightly so, failing)

msprotz commented 1 month ago

and the work is happening on branch protz_substitutions