Support `PartialOrd` and other generated things

[W95Psp]

For a bunch of "standard" derived core traits, we just ignore generated code.

• PartialOrd, Ord: straightforward, we might want lemmas saying that if x <= y and x >= y, then x == y, but this might not always be true (note: Ord vs PartialOrd, and is == Rust equality or theorem prover equality?)
• PartialEq, Eq: more complicated. It's perfectly fine to implement Eq and PartialEq to reflect equality on a partial view of a value.
• Debug: should be fairly easy
• Copy: implement as identity, it's only a marker-trait
• Clone: I think we still want to model clones as copies. A clone that is doing something more than cloning sub-values usually means it's doing a side effect (e.g. Rc).

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Still relevant, we discussed that recently with @maximebuyse

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

@maximebuyse can you look at it?

[maximebuyse]

I looked at the current behaviour, and I don't think anything changed since this issue was opened. We make derived trait impls opaque. So this issue is still fully relevant.

[clementblaudeau]

Will probably be addressed when porting the importer to rust