Commit 2026-05-28 08:23 f6d13193
View on Github →feat(Tactic/ToFun): warn if provided name matches autogenerated one (#39598)
This PR advises the user to remove a name they explicitly provided to @[to_fun] if it matches the name @[to_fun] would autogenerate.