mathlib

b01d6eb9 - fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument (#19228)

fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument (#19228) I found this bug during the porting. The current deriving handler doesn't work for this. ```lean @[derive [traversable,is_lawful_traversable]] inductive my_tree' (α : Type) | leaf : my_tree' | node : my_tree' → α → my_tree' → my_tree' ``` This is because the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument. Fortunatelly, the cause of this bug is just a mistake of the argument in `control.traversable.derive`.