Basic
📁 Source: Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsExprInfo, bvars, cfg, expr, lctx, localInsts, Key, arity, format, hash, LazyEntry, computedKeys, format, labelledStars?, mctx, previous, stack, StackEntry, format, Trie, children, labelledStars, pending, values, TrieIndex, format, go, instBEqKey, beq, instHashableKey, instInhabitedKey, default, instInhabitedLazyEntry, default, instInhabitedTrie, instToFormat, instToFormatKey, instToFormatLazyEntry, instToFormatStackEntry, keysAsPattern, go, mkApp, next, parenthesize, mkExprInfo, mkInitLazyEntry, root, tries, instInhabitedRefinedDiscrTree, default | 50 |
| Theorems | 0 |
| Total | 50 |
Lean.Meta
Definitions
| Name | Category | Theorems |
|---|---|---|
instInhabitedRefinedDiscrTree 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree
Definitions
| Name | Category | Theorems |
|---|---|---|
ExprInfo 📖 | CompData | — |
Key 📖 | CompData | — |
LazyEntry 📖 | CompData | — |
StackEntry 📖 | CompData | — |
Trie 📖 | CompData | — |
TrieIndex 📖 | CompOp | — |
format 📖 | CompOp | — |
instBEqKey 📖 | CompOp | — |
instHashableKey 📖 | CompOp | — |
instInhabitedKey 📖 | CompOp | — |
instInhabitedLazyEntry 📖 | CompOp | — |
instInhabitedTrie 📖 | CompOp | — |
instToFormat 📖 | CompOp | — |
instToFormatKey 📖 | CompOp | — |
instToFormatLazyEntry 📖 | CompOp | — |
instToFormatStackEntry 📖 | CompOp | — |
keysAsPattern 📖 | CompOp | — |
mkExprInfo 📖 | CompOp | — |
mkInitLazyEntry 📖 | CompOp | — |
root 📖 | CompOp | — |
tries 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.ExprInfo
Definitions
| Name | Category | Theorems |
|---|---|---|
bvars 📖 | CompOp | — |
cfg 📖 | CompOp | — |
expr 📖 | CompOp | — |
lctx 📖 | CompOp | — |
localInsts 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.Key
Definitions
| Name | Category | Theorems |
|---|---|---|
arity 📖 | CompOp | — |
format 📖 | CompOp | — |
hash 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.LazyEntry
Definitions
| Name | Category | Theorems |
|---|---|---|
computedKeys 📖 | CompOp | — |
format 📖 | CompOp | — |
labelledStars? 📖 | CompOp | — |
mctx 📖 | CompOp | — |
previous 📖 | CompOp | — |
stack 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.StackEntry
Definitions
| Name | Category | Theorems |
|---|---|---|
format 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.Trie
Definitions
| Name | Category | Theorems |
|---|---|---|
children 📖 | CompOp | — |
labelledStars 📖 | CompOp | — |
pending 📖 | CompOp | — |
values 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.format
Definitions
| Name | Category | Theorems |
|---|---|---|
go 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.instBEqKey
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.instInhabitedKey
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Lean.Meta.RefinedDiscrTree.keysAsPattern
Definitions
| Name | Category | Theorems |
|---|---|---|
go 📖 | CompOp | — |
mkApp 📖 | CompOp | — |
next 📖 | CompOp | — |
parenthesize 📖 | CompOp | — |
Lean.Meta.instInhabitedRefinedDiscrTree
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---