Lucas Franceschino
Lucas Franceschino
Seems like I can't reproduce any longer: ```rust trait T: Clone { type U: Clone; } impl T for () { type U = (); } fn f() {} ```...
PR https://github.com/hacspec/hax/pull/559 made some progress toward this issue, but we need to improve it to close this.
We wanted to work on that together in CC, but that will not happen this week (I thought I could do CC today, but after being awake for a bit,...
In more details, the work around is: ```rust struct Foo(u8); impl std::ops::Index for Foo { type Output = u8; fn index(&self, idx: ()) -> &u8 { &self.0 } } #[hax_lib::exclude]...
We have a workaround, but we should still be able to support those directly.
For now, the workaround is to use `hax_lib::assert!` instead of std's `assert!`
Yes, you are right, hax should already handle basic rewriting when it's possible. I'm gonna try to allocate some time to that somewhere next week!
Fixed by #988
This is closed, the regression is tracked by https://github.com/hacspec/hax/issues/1044, and is going to be fixed soon.
@cmester0, is that still an issue or it's supported now?