Documentation Verification Report

PremiseIndex

📁 Source: Aesop/Forward/PremiseIndex.lean

Statistics

Metric	Count
Definitions `PremiseIndex`, `toNat`, `instBEqPremiseIndex`, `beq`, `instDecidableEqPremiseIndex`, `decEq`, `instDecidableRelPremiseIndexLe`, `instDecidableRelPremiseIndexLt`, `instHashablePremiseIndex`, `hash`, `instInhabitedPremiseIndex`, `default`, `instLEPremiseIndex`, `instLTPremiseIndex`, `instOrdPremiseIndex`, `ord`, `instToStringPremiseIndex`	17
Theorems	0
Total	17

Aesop

Definitions

Name	Category	Theorems
`PremiseIndex` 📖	CompData	—
`instBEqPremiseIndex` 📖	CompOp	—
`instDecidableEqPremiseIndex` 📖	CompOp	—
`instDecidableRelPremiseIndexLe` 📖	CompOp	—
`instDecidableRelPremiseIndexLt` 📖	CompOp	—
`instHashablePremiseIndex` 📖	CompOp	—
`instInhabitedPremiseIndex` 📖	CompOp	—
`instLEPremiseIndex` 📖	CompOp	—
`instLTPremiseIndex` 📖	CompOp	—
`instOrdPremiseIndex` 📖	CompOp	—
`instToStringPremiseIndex` 📖	CompOp	—

Aesop.PremiseIndex

Definitions

Name	Category	Theorems
`toNat` 📖	CompOp	—

Aesop.instBEqPremiseIndex

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Aesop.instDecidableEqPremiseIndex

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Aesop.instHashablePremiseIndex

Definitions

Name	Category	Theorems
`hash` 📖	CompOp	—

Aesop.instInhabitedPremiseIndex

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instOrdPremiseIndex

Definitions

Name	Category	Theorems
`ord` 📖	CompOp	—

---

← Back to Index