Nadrieril
Nadrieril
I'm working onremoving the need for `rustup`
Btw, rustup should no longer be needed
Actually, why not add `charon` to the dev shell? You'd have to find a way to male `charon-ml` available to opam. The idea being that someone who only wants to...
Oh you're right, I was thinking of aeneas devs but this PR is for aeneas users. Nevermind
Oh yeah this needs latest charon; I'll bump soon
We can likely replace all `Copy` bounds with `Clone` bounds, but is that an improvement? Your type signature would stay roughly the same
Maybe a `--discard-unused-bounds` flag on Charon would make sense, under which we could often remove the `Copy` bounds altogether
Or normalization could just ignore those builtins, so that you can further normalize it later with a different implementation that does support the builtin ? Not a common usecase though.
Noting here that I no longer think we need the "`&` everywhere" part of the proposal. This makes the proposed fix less local but saves us in design and possible...