LevelIndex

📁 Source: Aesop/Forward/LevelIndex.lean

Statistics

Metric	Count
Definitions LevelIndex, toNat, instBEqLevelIndex, beq, instDecidableEqLevelIndex, decEq, instDecidableRelLevelIndexLe, instDecidableRelLevelIndexLt, instHashableLevelIndex, hash, instInhabitedLevelIndex, default, instLELevelIndex, instLTLevelIndex, instOrdLevelIndex, ord, instToStringLevelIndex	17
Theorems	0
Total	17

Aesop

Definitions

Name	Category	Theorems
LevelIndex 📖	CompData	—
instBEqLevelIndex 📖	CompOp	—
instDecidableEqLevelIndex 📖	CompOp	—
instDecidableRelLevelIndexLe 📖	CompOp	—
instDecidableRelLevelIndexLt 📖	CompOp	—
instHashableLevelIndex 📖	CompOp	—
instInhabitedLevelIndex 📖	CompOp	—
instLELevelIndex 📖	CompOp	—
instLTLevelIndex 📖	CompOp	—
instOrdLevelIndex 📖	CompOp	—
instToStringLevelIndex 📖	CompOp	—

Aesop.LevelIndex

Definitions

Name	Category	Theorems
toNat 📖	CompOp	—

Aesop.instBEqLevelIndex

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Aesop.instDecidableEqLevelIndex

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Aesop.instHashableLevelIndex

Definitions

Name	Category	Theorems
hash 📖	CompOp	—

Aesop.instInhabitedLevelIndex

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instOrdLevelIndex

Definitions

Name	Category	Theorems
ord 📖	CompOp	—

---

← Back to Index