SlotIndex

📁 Source: Aesop/Forward/SlotIndex.lean

Statistics

Metric	Count
Definitions SlotIndex, toNat, instBEqSlotIndex, beq, instDecidableEqSlotIndex, decEq, instDecidableRelSlotIndexLe, instDecidableRelSlotIndexLt, instHAddSlotIndexNat, instHSubSlotIndexNat, instHashableSlotIndex, hash, instInhabitedSlotIndex, default, instLESlotIndex, instLTSlotIndex, instOrdSlotIndex, ord, instToStringSlotIndex	19
Theorems	0
Total	19

Aesop

Definitions

Name	Category	Theorems
SlotIndex 📖	CompData	—
instBEqSlotIndex 📖	CompOp	—
instDecidableEqSlotIndex 📖	CompOp	—
instDecidableRelSlotIndexLe 📖	CompOp	—
instDecidableRelSlotIndexLt 📖	CompOp	—
instHAddSlotIndexNat 📖	CompOp	—
instHSubSlotIndexNat 📖	CompOp	—
instHashableSlotIndex 📖	CompOp	—
instInhabitedSlotIndex 📖	CompOp	—
instLESlotIndex 📖	CompOp	—
instLTSlotIndex 📖	CompOp	—
instOrdSlotIndex 📖	CompOp	—
instToStringSlotIndex 📖	CompOp	—

Aesop.SlotIndex

Definitions

Name	Category	Theorems
toNat 📖	CompOp	—

Aesop.instBEqSlotIndex

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Aesop.instDecidableEqSlotIndex

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Aesop.instHashableSlotIndex

Definitions

Name	Category	Theorems
hash 📖	CompOp	—

Aesop.instInhabitedSlotIndex

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.instOrdSlotIndex

Definitions

Name	Category	Theorems
ord 📖	CompOp	—

---

← Back to Index