Lucas Franceschino
Lucas Franceschino
Hi @paulmure, I've been trying to review a few times, but each time I end up wondering if that's the right thing to do. I agree with you, the view...
Yeah. I see what you mean. Indeed, we may end up with a messy and complicated API... The implementation itself is already quite messy and complicated, actually 😅 I would...
A nice encoding in F* could be as follows: ```fstar noeq type dyn (traits: Type0 -> Type) = { typ: Type0 ; value: typ ; interfaces: traits typ } ```...
I suspect that's the same issue as https://github.com/hacspec/hax/issues/683
Hi, as we discussed on [Zulip yesterday](https://hacspec.zulipchat.com/#narrow/stream/269544-general/topic/Issues.20with.20the.20importer), I think getting rid of this `NonImplementedYet` variant would be great! If you need any pointers or help for adding those, tell us...
That was still relevant, the bot was too quick
Still relevant
Related to #108
This is still the case, with: ```rust error[E9999]: Cannot handle error `Unimplemented` selecting `Binder { value: , bound_vars: [] }` --> literals/src/lib.rs:4:1 | 4 | trait Bar {} | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
This was silenced as a warning by PR #898, but this is still an issue.