Basic
📁 Source: Aesop/Index/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsIndexMatchLocation, instBEq, instHashable, instOrd, instToMessageData, IndexMatchResult, instLTOfOrd, instOrd, instToMessageData, locations, patternSubsts?, rule, IndexingMode, format, hypsMatchingConst, instToFormat, targetMatchingConclusion, instInhabitedIndexMatchLocation, default, instInhabitedIndexMatchResult, default, instInhabitedIndexingMode, default | 23 |
| Theorems | 0 |
| Total | 23 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
IndexMatchLocation 📖 | CompData | — |
IndexMatchResult 📖 | CompData | — |
IndexingMode 📖 | CompData | — |
instInhabitedIndexMatchLocation 📖 | CompOp | — |
instInhabitedIndexMatchResult 📖 | CompOp | — |
instInhabitedIndexingMode 📖 | CompOp | — |
Aesop.IndexMatchLocation
Definitions
| Name | Category | Theorems |
|---|---|---|
instBEq 📖 | CompOp | — |
instHashable 📖 | CompOp | — |
instOrd 📖 | CompOp | — |
instToMessageData 📖 | CompOp | — |
Aesop.IndexMatchResult
Definitions
| Name | Category | Theorems |
|---|---|---|
instLTOfOrd 📖 | CompOp | — |
instOrd 📖 | CompOp | — |
instToMessageData 📖 | CompOp | — |
locations 📖 | CompOp | — |
patternSubsts? 📖 | CompOp | — |
rule 📖 | CompOp | — |
Aesop.IndexingMode
Definitions
| Name | Category | Theorems |
|---|---|---|
format 📖 | CompOp | — |
hypsMatchingConst 📖 | CompOp | — |
instToFormat 📖 | CompOp | — |
targetMatchingConclusion 📖 | CompOp | — |
Aesop.instInhabitedIndexMatchLocation
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedIndexMatchResult
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedIndexingMode
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---