Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Data/Tree: Add Traversable instance. #13572

Open
Tracked by #7987
BoltonBailey opened this issue Jun 6, 2024 · 1 comment
Open
Tracked by #7987

Data/Tree: Add Traversable instance. #13572

BoltonBailey opened this issue Jun 6, 2024 · 1 comment
Labels
enhancement New feature or request good first issue Good for newcomers

Comments

@BoltonBailey
Copy link
Collaborator

BoltonBailey commented Jun 6, 2024 •
edited by Komyyy
Loading

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.
@BoltonBailey BoltonBailey mentioned this issue Jun 6, 2024
Open
@BoltonBailey BoltonBailey added good first issue Good for newcomers enhancement New feature or request labels Jun 6, 2024
@Komyyy
Copy link
Collaborator

Komyyy commented Jun 8, 2024

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

@Komyyy Komyyy changed the title Data/Tree: Add Traversible instance. Data/Tree: Add Traversable instance. Jul 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@BoltonBailey @Komyyy