Commit 2026-09-19 18:24 0acbe13e

View on Github →

feat(Translate): improve error message when translation fails (#42400) This PR improves the error message to_additive/to_dual gives when the translation fails. In particular, it was previously possible to get a kernel error when the value itself was type correct, but it didn't match with the translated type. This PR also takes the opportunity to handle private and exposed more carefully. So, the new error messages will come from checks at the right exporting level. I've also added tests showing that to_additive deals with private and exposed correctly. To do this, the to_additive test file was made into a module.

Estimated changes

modified def Test.MonoidEnd
modified theorem Test.bar10_works
modified theorem Test.bar11_works
deleted def Test.checkGuessName
modified theorem Test.foo15
modified theorem Test.foo4_test
added theorem mul_rfl