Nadrieril
Nadrieril
Any help here is needed. I'm more than happy to fill holes with the knowledge I have, what's difficult for me is getting started on what needs to be explained...
Hehe let me propagate the curse. Fun fact, [this](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=bb39aec4acae80b02b89b74d6b2ca98a) trips Miri (because we sort or-patterns last for perf reasons): ```rust unsafe fn tag_first(v: Tagged) -> bool { match v {...
Yeah I marked it as draft because it doesn't work for complex cases such as destructuring or `assert!` that you test in Eurydice
I was hoping to get back to it when higher-priority items are done, but tbf I don't know how to go about this. The few heuristics I tried don't work...
I don't know of anyone else doing that no
r? @Urgau since you seem interested in solving this
Should I edit the OP? I'm not sure how this works.
With https://github.com/AeneasVerif/charon/pull/316, `charon --include "core::convert::{impl core::convert::Into for _}::into"` will translate precisely the requested method. This avoids the issue of `--extract-opaque-bodies` extracting too much.
the rust name matcher doesn't actually handle inherent impl blocks at all at the moment :sweat_smile:
I can't distinguish impl blocks from trait impls because we allow `{Trait}` syntax