Lucas Franceschino
Lucas Franceschino
The first snippet of code is failing to extract because the type of `bytes[0]` is an associated type. For now, Hax is not able to look those up. Though, associated...
Yes, that's the long-standing #20 issue
(well, we had support for traits via typeclass resolution in the backends, but we had no pre-resolved instance info :smiley:)
Update on that: Now we have associated types correctly resolved, this bug still persist, and is related to to the way `x = e` is desugared in [import thir]( https://github.com/hacspec/hax/blob/eebfe9b38a621d924794379553a9b263ba7d32bd/engine/lib/import_thir.ml#L499-L501C11)....
Let's close in favor of https://github.com/hacspec/hax/issues/491
It is probably related to https://github.com/hacspec/hax/issues/231
Should we merge this, now https://github.com/hacspec/hax/pull/856 is in (aka unsize are gone)?
Seems like this was merged into https://github.com/cryspen/libcrux/pull/475
Nice, let's close this, there are a few thing, gonna make another PR
[removed] See https://github.com/cryspen/home/issues/274 instead.