Nadrieril

I like "iter_enumerated", that's what https://doc.rust-lang.org/nightly/nightly-rustc/rustc_index/struct.IndexVec.html uses

Notes: [this](https://github.com/AeneasVerif/aeneas/blob/24fc188af7032b8119cb7504965b82216e2bbf6b/compiler/Translate.ml#L1155) is where we copy the files; [this](https://github.com/AeneasVerif/aeneas/blob/24fc188af7032b8119cb7504965b82216e2bbf6b/compiler/Translate.ml#L868) is where we generate headers.

That's weird, it's trying to compile charon with a stable compiler which is guaranteed to fail. Can you `rm -rf charon; gmake setup-charon` and paste the complete output of that?

Interesting, I was not aware of that! I thought PlaceMention was removed in runtime MIR but looking through rustc I see a `-Zmir-preserve-ub` flag that keeps it! So I agree...

For many years you could write `(x: Type)` in a pattern on nightly. I think that was never implemented fully and ended up being removed but sounds like this is...

Could the `Captures` trait make it into std so that rustc can suggest it? It's otherwise impossible to discover this trick but it's a very useful one.

Can you try `--cargo-arg '--package=serde'` (with an appropriate package name)?

I can confirm that works, so this is so far cargo working as expected. We'll have to investigate to see if we can ask it to translate all crates in...

For this issue, the first step would be to add a test to `tests/cargo` that has a virtual manifest and exhibits this error. Second step would be to somehow ask...

We can't have lists of types, because we'd need `[Bool, (Natural -> Natural)] : List Type`, but `List Type` doesn't typecheck. The reason is that `List` has type `Type ->...