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 of applyReplacementFun. The current situation requires uses of applyReplacementFun to know that they need to call expand 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 in dontTranslate, it would do the wrong thing (although I don't think this will ever come up in practice)

Estimated changes