Datatypes
📁 Source: Mathlib/Tactic/Explode/Datatypes.lean
Statistics
| Metric | Count |
|---|---|
| 21 | |
| Theorems | 0 |
| Total | 21 |
Mathlib.Explode
Definitions
| Name | Category | Theorems |
|---|---|---|
Entries 📖 | CompData | — |
Entry 📖 | CompData | — |
Status 📖 | CompData | — |
instInhabitedEntries 📖 | CompOp | — |
instInhabitedStatus 📖 | CompOp | — |
Mathlib.Explode.Entries
Definitions
| Name | Category | Theorems |
|---|---|---|
add 📖 | CompOp | — |
addSynonym 📖 | CompOp | — |
find? 📖 | CompOp | — |
l 📖 | CompOp | — |
s 📖 | CompOp | — |
size 📖 | CompOp | — |
Mathlib.Explode.Entry
Definitions
| Name | Category | Theorems |
|---|---|---|
deps 📖 | CompOp | — |
depth 📖 | CompOp | — |
line 📖 | CompOp | — |
line! 📖 | CompOp | — |
status 📖 | CompOp | — |
thm 📖 | CompOp | — |
type 📖 | CompOp | — |
useAsDep 📖 | CompOp | — |
Mathlib.Explode.instInhabitedEntries
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Explode.instInhabitedStatus
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---