Commit 2026-06-08 18:33 eaa4d409

View on Github →

chore(Data/Tree/Basic): Rename Tree to BinaryTree (#39707) Rename Tree to BinaryTree. This frees up the name Tree to cover n-ary trees in future. We only deprecate the defs, and move the theorems without deprecation.

Estimated changes

modified def DyckWord.equivTree
modified def DyckWord.ofTree
modified def DyckWord.toTree
added theorem BinaryTree.comp_map
added theorem BinaryTree.id_map
added def BinaryTree.left
added def BinaryTree.map
added def BinaryTree.right
added inductive BinaryTree.{u}
deleted theorem Tree.comp_map
deleted def Tree.height
deleted theorem Tree.height_le_numNodes
deleted theorem Tree.id_map
deleted def Tree.left
deleted def Tree.map
deleted def Tree.numLeaves
deleted theorem Tree.numLeaves_pos
deleted def Tree.numNodes
deleted def Tree.right
deleted def Tree.traverse
deleted theorem Tree.traverse_pure
deleted def Tree.unitRecOn
deleted inductive Tree.{u}
added def BinaryTree.get
deleted def Tree.get
deleted def Tree.getOrElse
deleted def Tree.indexOf
added theorem BinaryTree.naturality
deleted theorem Tree.comp_traverse
deleted theorem Tree.naturality
deleted theorem Tree.traverse_eq_map_id