Lucas Franceschino
Lucas Franceschino
Ok, I'm in a rush and so I rushed the review as well... I wanted to merge too fast, and actually I think there is a problem with the PR....
Hi @paulmure, I'm reviewing this PR this morning, and I think I did something similar recently... https://github.com/hacspec/hax/pull/827 Sorry for the duplicate work... (the last month has been pretty work intensive...
Here is a slightly minimized version: ```rust #[allow(dead_code)] fn f(f: impl FnOnce(()) -> ()) {} /// The following `into` is (wrongly) extracted as `Core.Convert.Into.into` fn g() { f(Into::into) } ///...
Would still be useful
Let's keep open, related to https://github.com/cryspen/hax-evit/issues/11
Still relevant
Still relevant
That's still relevant, and something we need for what @cmester0 is busy with (core). https://rust-lang.github.io/rfcs/2603-rust-symbol-name-mangling-v0.html is super interesting, but overkill for us: we don't need to recover full Rust names...
We still need this phase: rewrite control flow introduces too many deduplication in certain case.
For now I came up with something like this, but that's not OK, we want to be able to refine nested types (ie a slice of refined something) ``` #[hax_lib::define_named_refinement]...