Commit 2023-02-04 00:58 722b01f8

View on Github →

fix: interaction between to_additive and rewriting definitions (#1948)

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Expr.listNamesWithPrefixes

added def Lean.Name.isPrefixOf?

Modified Mathlib/Tactic/ToAdditive.lean

added def ToAdditive.findAuxDecls

added def ToAdditive.findTargetName

Modified test/toAdditive.lean

added theorem Test.npowRec_zero

added theorem Test.optiontest