Initialize

📁 Source: Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean

Statistics

Metric	Count
Definitions ModuleDiscrTreeRef, ref, PreDiscrTree, append, instAppend, root, toRefinedDiscrTree, tries, blacklistInsertion, createImportedDiscrTree, createModuleDiscrTree, createModuleTreeRef, insert, instInhabitedPreDiscrTree, default	15
Theorems	0
Total	15

Lean.Meta.RefinedDiscrTree

Definitions

Name	Category	Theorems
ModuleDiscrTreeRef 📖	CompData	—
PreDiscrTree 📖	CompData	—
blacklistInsertion 📖	CompOp	—
createImportedDiscrTree 📖	CompOp	—
createModuleDiscrTree 📖	CompOp	—
createModuleTreeRef 📖	CompOp	—
insert 📖	CompOp	—
instInhabitedPreDiscrTree 📖	CompOp	—

Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef

Definitions

Name	Category	Theorems
ref 📖	CompOp	—

Lean.Meta.RefinedDiscrTree.PreDiscrTree

Definitions

Name	Category	Theorems
append 📖	CompOp	—
instAppend 📖	CompOp	—
root 📖	CompOp	—
toRefinedDiscrTree 📖	CompOp	—
tries 📖	CompOp	—

Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index