Commit 2025-01-23 16:30 fe0ee9b2

View on Github →

feat(Data/Control/Traversable/Instances): Add (Lawful)Traversable instance for Tree (#18818) This PR completes a TODO; this PR closes #13572. It was suggested at the issue that this could also be done with the derive handler for (Lawful)Traversable, but as mentioned there, that generates map and traverse functions that are not as universe-polymorphic. For writing the Lawful proof i took inspiration from the same instance for FreeMagma

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Tree/Basic.lean

added theorem Tree.comp_map

added theorem Tree.id_map

added def Tree.traverse

added theorem Tree.traverse_pure

Created Mathlib/Data/Tree/Traversable.lean

added theorem Tree.comp_traverse

added theorem Tree.naturality

added theorem Tree.traverse_eq_map_id