Trees

InductiveTree#

A binary tree with values stored in non-leaf nodes.

BinaryTree.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: BinaryTree
• Source of BinaryTree in Mathlib/Data/Tree/Basic.lean
• Mathlib overview: Data structures › Trees

MathlibBinaryTree

InductiveSize-balanced binary search tree#

An Ordnode α is a finite set of values, represented as a tree. The operations on this type maintain that the tree is balanced and correctly stores subtree sizes at each level.

This is a copy of BinaryTree with a cached size field for BinaryTree.numNodes.

Ordnode.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: Ordnode
• Source of Ordnode in Mathlib/Data/Ordmap/Ordnode.lean
• Mathlib overview: Data structures › Trees

MathlibOrdnode

Uses 1 · Used by 1

Statement usesNatural number

Used byOrdered set

InductiveW type#

Given β : α → Type*, WType β is the type of finitely branching trees where nodes are labeled by elements of α and the children of a node labeled a are indexed by elements of β a.

WType.{u_1, u_2} {α : Type u_1} (β : α → Type u_2) : Type (max u_1 u_2)

Sources

• Mathlib documentation: WType
• Source of WType in Mathlib/Data/W/Basic.lean
• Mathlib overview: Data structures › Trees

MathlibWType

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.