Export
📁 Source: Mathlib/Util/Export.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsAlloc, map, next, Entry, OfState, get, modify, defs, exprs, levels, names, stk, alloc, biStr, exportDef, exportExpr, exportLevel, exportName, instCoeExprEntry, instCoeLevelEntry, instCoeNameEntry, instInhabitedAlloc, default, instInhabitedEntry, default, instInhabitedState, default, instOfStateExpr, instOfStateLevel, instOfStateName, runExportM, ExportM | 32 |
| Theorems | 0 |
| Total | 32 |
Lean
Definitions
| Name | Category | Theorems |
|---|---|---|
ExportM 📖 | CompOp | — |
Lean.Export
Definitions
| Name | Category | Theorems |
|---|---|---|
Alloc 📖 | CompData | — |
Entry 📖 | CompData | — |
OfState 📖 | CompData | — |
alloc 📖 | CompOp | — |
biStr 📖 | CompOp | — |
exportDef 📖 | CompOp | — |
exportExpr 📖 | CompOp | — |
exportLevel 📖 | CompOp | — |
exportName 📖 | CompOp | — |
instCoeExprEntry 📖 | CompOp | — |
instCoeLevelEntry 📖 | CompOp | — |
instCoeNameEntry 📖 | CompOp | — |
instInhabitedAlloc 📖 | CompOp | — |
instInhabitedEntry 📖 | CompOp | — |
instInhabitedState 📖 | CompOp | — |
instOfStateExpr 📖 | CompOp | — |
instOfStateLevel 📖 | CompOp | — |
instOfStateName 📖 | CompOp | — |
runExportM 📖 | CompOp | — |
Lean.Export.Alloc
Definitions
| Name | Category | Theorems |
|---|---|---|
map 📖 | CompOp | — |
next 📖 | CompOp | — |
Lean.Export.OfState
Definitions
| Name | Category | Theorems |
|---|---|---|
get 📖 | CompOp | — |
modify 📖 | CompOp | — |
Lean.Export.State
Definitions
| Name | Category | Theorems |
|---|---|---|
defs 📖 | CompOp | — |
exprs 📖 | CompOp | — |
levels 📖 | CompOp | — |
names 📖 | CompOp | — |
stk 📖 | CompOp | — |
Lean.Export.instInhabitedAlloc
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Lean.Export.instInhabitedEntry
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Lean.Export.instInhabitedState
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---