Commit 2025-04-08 19:26 68c6e4e1

View on Github →

chore(WithOne): review (#23837)

  • Drop a duplicate Repr instance for WithZero.
  • Rename instances from myclass to instMyclass.
  • Use better names for the recursor arguments.

Estimated changes

modified def WithOne.recOneCoe
modified theorem WithOne.recOneCoe_coe
modified theorem WithOne.recOneCoe_one