Commit 2026-10-04 05:36 6066db18

feat(Translate): implementation of to_dual_for command (#44270) This PR introduced to_dual_for, a command that adds a translation for a given constant. It gives two benefits:

• When a translation has to be added just to make to_dual work, it is much more convenient to do so with to_dual_for
• When you want to translate a definition to another definition but this is not possible because a proof argument does not match up, you can now use to_dual_for to do the translation, which was previously not possible. This is because to_dual_for lets you translate to an arbitrary expression, rather than to a constant. This is in particular useful for Cone.ext/Cocone.ext