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:
expand
is moved up so that it can be called directly inside ofapplyReplacementFun
. The current situation requires uses ofapplyReplacementFun
to know that they need to callexpand
first.applyReplacementFun
is 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
reorder
would reorder some argument that appears indontTranslate
, it would do the wrong thing (although I don't think this will ever come up in practice)