Nadrieril
Nadrieril
> What doesn't typecheck? I don't see any issue in the diffs or in CI. That's because I just fixed it :) I had messed up the self clauses and...
> at some point I thought of making the default methods take as inputs exactly the list of functions they need Yes we discussed this together :p
The old monomorphization pass has been removed. The new one does also have some generics bugs, from the looks of it just a detail in `BuiltinOrAuto` most likely coming from...
First step for that is #864. Second step would be to make `FunDeclId` into an enum ```rust enum FunDeclId { Intrinsic(Intrinsic), Indexed(usize), } ``` so that users can choose to...
Imo we should remove that parameter in a micro-pass instead. I saw a TODO to this effect somewhere recently.
For context, the llbc for that is: ``` trait core::convert::From { fn from : core::convert::From::from } trait core::convert::Into { fn into : core::convert::Into::into } fn core::convert::{impl core::convert::Into for T#3}::into(@1: T)...
This imports the very generic impl: ```rust impl Into for T where U: From, { ... } ``` My guess is that the name you generate for that is `core.convert.Into`...
I don't know I couldn't try because of ocaml version mismatches
First big chunk was done here: https://github.com/AeneasVerif/charon/pull/283
This is pretty much done now