search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.19k stars 257 forks source link

Data/Tree: Add `Traversable` instance. #13572

Open BoltonBailey opened 1 month ago

BoltonBailey commented 1 month ago

The Tree type defined in Mathlib/Data/Tree.lean should have a Traversable instance. This should be added to the file and the associated TODO removed.

Komyyy commented 1 month ago

@BoltonBailey Last year, I ported the LawfulTraversable instance deriver which derives Traversable attendantly in Mathlib.Tactic.DeriveTraversable. You can see the example in test.Traversable. This instance deriver should help you. 😄