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

[Komyyy]

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.

---

[eric-wieser]

It's pretty hard to follow what this code is doing, but the correction certainly looks plausible, and the test passes.

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests