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

Closed

[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 #19228

Komyyy wants to merge 1 commit into master from Komyyy/control.traversable.derive

fix

f517fb9e

Komyyy added bug

Komyyy added awaiting-review

Komyyy added awaiting-CI

Komyyy added easy

Komyyy removed easy

github-actions removed awaiting-CI

eric-wieser added t-meta

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument~~ [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 2 years ago

bors closed this 2 years ago

bors deleted the Komyyy/control.traversable.derive branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

bug ready-to-merge t-meta

Milestone

No milestone

mathlib3 [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 #19228 Closed

[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 #19228

mathlib3
[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
#19228

Closed