Nadrieril
Nadrieril
This looks good for me, could someone with authority approve this plz?
EDIT: nevermind, moved this to another issue
> If so, what are the next steps to get it started? No one answered, but the answer is "add the I-lang-nominated label and wait for the lang team to...
Another fun one: ```rust trait A {} struct B where B: A { t: T } ```
I think for the most part this requires tracking items not by name (RPITIT items don't have a name) but by some new id. I'm thinking `AssocTyId`/`AssocConstId`/`MethodId` for the various...
I intend this for all names. I also intend for the name matcher to optionally work on short names (and raise an error if there could be ambiguity).
We can also easily add an option to print full names, or add a map from short to full names in the llbc output.
Agreed, hence why "optional". I also think short names are a lot more convenient when prototyping so it's a good option to have.
https://github.com/hacspec/hax/pull/1215 fixes some of the first kind of error but not yet all. I left [a hack](https://github.com/Nadrieril/hax/blob/79e2da0452a0b94056becba46b98304ca230a502/frontend/exporter/src/types/new/full_def.rs#L808-L815) that we'll be able to remove after #127.
This happens in particular in the stdlib, for the `Iterator::fold` impl of `slice::Iter`.