Automatic derivation on the backend side for extracted data types

AeneasVerif / aeneas

A verification toolchain for Rust programs

Apache License 2.0

167 stars 15 forks source link

Automatic derivation on the backend side for extracted data types #224

Open RaitoBezarius opened 1 month ago

RaitoBezarius commented 1 month ago

Lean supports automatic derivation of Repr and potential other typeclasses, it seems cheap to derive them.

Question is: are there situations where a user doesn't want additional typeclasses attached to their extracted data types?

RaitoBezarius commented 1 month ago

cc @R1kM @sonmarcho

sonmarcho commented 1 month ago

For now I don't see situations where a user seriously doesn't want additional typeclasses, so I suggest we implement this. The real questions is: which typeclasses do we want? Also, are there situations where Lean will fail to derive the typeclasses?