Commit 2023-03-12 12:39 c1167dd0

View on Github →

feat: Port Data.Tree (#2587)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Tree.lean

added def Tree.get

added def Tree.getOrElse

added def Tree.height

added theorem Tree.height_le_numNodes

added def Tree.indexOf

added def Tree.left

added theorem Tree.left_node_right_eq_self

added def Tree.map

added def Tree.numLeaves

added theorem Tree.numLeaves_eq_numNodes_succ

added theorem Tree.numLeaves_pos

added def Tree.numNodes

added def Tree.ofRBNode

added def Tree.recOnC

added theorem Tree.recOn_Unit_eq_recOnC

added def Tree.right

added def Tree.unitRecOn

added inductive Tree.{u}