Son HO
Son HO
Using attributes to indicate the effect is indeed a general, modular way of directing the translation. And I agree with the idea of annotating trait definitions, or rather trait methods....
> > triggering the simplification with attributes only > > One difficulty here would be for functions in external dependencies, which would not be possible/easy to annotate. Yes, that's an...
> I like the idea of using attributes, as this also paves the way towards more expressive "effects". Regarding your idea of simplifying through micro-passes in the pure model, wouldn't...
> What happens if the simplification criterion gets improved and starts detecting more functions? Would this break proofs that depended on the previous behavior? Yes, it will likely break proofs....
We can consider this as done, right?
This PR seems dead, so I'm closing it. Feel free to reopen it if you really want this feature.
Thanks for this! Indeed, `progress` doesn't expect to see an implication, so maybe we need to generalize it a bit (or at least print a nice error message).
This comes from the fact that for now we do not allow overriding default methods in trait implementations, because it makes the code generation quite hard (and according to the...
I'm currently cleaning the issues and removing duplicates: I updated the name of the issue.
The following code also triggers the same issue (comes from https://github.com/AeneasVerif/aeneas/issues/71): ```rust fn main() { let x = 1; let _ = &x == &1; } ```