Commit 2023-07-12 18:27 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) I found this bug during the porting. The current deriving handler doesn't work for this.

@[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.