Def Tree.indexOf

Modification history

2026-06-08 18:33

Mathlib/Data/Tree/Get.lean

chore(Data/Tree/Basic): Rename Tree to BinaryTree (#39707) …

Deleted Tree.indexOf View on Github →

2024-06-08 18:34

Mathlib/Data/Tree/Basic.lean

chore(Data/Tree): split file (#13629) …

Modified Tree.indexOf View on Github →

2023-03-12 12:39

Mathlib/Data/Tree.lean

feat: Port Data.Tree (#2587)

Added Tree.indexOf View on Github →