Commit 2025-09-23 18:21 8e82ec6c
View on Github →fix(Tactic/ToAdditive/Frontend): swap reorderForall and applyReplacementForall (#29119)
This PR does some general clean-up in the to_additive implementation:
expandis moved up so that it can be called directly inside ofapplyReplacementFun. The current situation requires uses ofapplyReplacementFunto know that they need to callexpandfirst.applyReplacementFunis significantly cleaned up, without changing the implementation, making it shorter, more readable and more efficient.- It swaps reorderForall/Lambda with applyReplacementForall/Lambda, because in the previous order, if
reorderwould reorder some argument that appears indontTranslate, it would do the wrong thing (although I don't think this will ever come up in practice)