Commit 2025-12-04 17:49 fab0e3f3
View on Github →fix(to_additive): use findRelevantArg for auxiliarly declarations (#32404)
This PR uses the heuristic findRelevantArg for determining the relevant_arg in auxiliary declarations. Previously, it was always set to the default 1 in auxiliary declarations.
Future work: findRelevantArg is somewhat limited in its ability to recognize the correct relevant_arg. It may be improved in the future (together with a linter that tells you when a (relevant_arg := ...) argument is already found by the heuristic)