structure Aesop.PremiseIndex : Type

• toNat : Nat

instance Aesop.instInhabitedPremiseIndex : Inhabited PremiseIndex

Equations

• Aesop.instInhabitedPremiseIndex = { default := { toNat := default } }

instance Aesop.instBEqPremiseIndex : BEq PremiseIndex

Equations

• Aesop.instBEqPremiseIndex = { beq := Aesop.beqPremiseIndex✝ }

instance Aesop.instHashablePremiseIndex : Hashable PremiseIndex

Equations

• Aesop.instHashablePremiseIndex = { hash := Aesop.hashPremiseIndex✝ }

instance Aesop.instDecidableEqPremiseIndex : DecidableEq PremiseIndex

Equations

• Aesop.instDecidableEqPremiseIndex = Aesop.decEqPremiseIndex✝

instance Aesop.instOrdPremiseIndex : Ord PremiseIndex

Equations

• Aesop.instOrdPremiseIndex = { compare := Aesop.ordPremiseIndex✝ }

instance Aesop.instLTPremiseIndex : LT PremiseIndex

Equations

• Aesop.instLTPremiseIndex = { lt := fun (i j : Aesop.PremiseIndex) => i.toNat < j.toNat }

instance Aesop.instDecidableRelPremiseIndexLt : DecidableRel fun (x1 x2 : PremiseIndex) => x1 < x2

Equations

• Aesop.instDecidableRelPremiseIndexLt i j = inferInstanceAs (Decidable (i.toNat < j.toNat))

instance Aesop.instLEPremiseIndex : LE PremiseIndex

Equations

• Aesop.instLEPremiseIndex = { le := fun (i j : Aesop.PremiseIndex) => i.toNat ≤ j.toNat }

instance Aesop.instDecidableRelPremiseIndexLe : DecidableRel fun (x1 x2 : PremiseIndex) => x1 ≤ x2

Equations

• Aesop.instDecidableRelPremiseIndexLe i j = inferInstanceAs (Decidable (i.toNat ≤ j.toNat))

instance Aesop.instToStringPremiseIndex : ToString PremiseIndex

Equations

• Aesop.instToStringPremiseIndex = { toString := fun (i : Aesop.PremiseIndex) => toString i.toNat }