← Copula mathematical handbook

structure Aesop.PremiseIndex : Type

• toNat : Nat

@[instance_reducible]

instance Aesop.instInhabitedPremiseIndex : Inhabited PremiseIndex

Equations

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

@[instance_reducible]

instance Aesop.instBEqPremiseIndex : BEq PremiseIndex

Equations

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

def Aesop.instBEqPremiseIndex.beq : PremiseIndex → PremiseIndex → Bool

Equations

• Aesop.instBEqPremiseIndex.beq { toNat := a } { toNat := b } = (a == b)
• Aesop.instBEqPremiseIndex.beq x✝¹ x✝ = false

@[instance_reducible]

instance Aesop.instHashablePremiseIndex : Hashable PremiseIndex

Equations

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

def Aesop.instHashablePremiseIndex.hash : PremiseIndex → UInt64

Equations

• Aesop.instHashablePremiseIndex.hash { toNat := a } = mixHash 0 (hash a)

def Aesop.instDecidableEqPremiseIndex.decEq (x✝ x✝¹ : PremiseIndex) : Decidable (x✝ = x✝¹)

Equations

• Aesop.instDecidableEqPremiseIndex.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aesop.instDecidableEqPremiseIndex : DecidableEq PremiseIndex

Equations

• Aesop.instDecidableEqPremiseIndex = Aesop.instDecidableEqPremiseIndex.decEq

@[instance_reducible]

instance Aesop.instOrdPremiseIndex : Ord PremiseIndex

Equations

• Aesop.instOrdPremiseIndex = { compare := Aesop.instOrdPremiseIndex.ord }

def Aesop.instOrdPremiseIndex.ord : PremiseIndex → PremiseIndex → Ordering

Equations

• Aesop.instOrdPremiseIndex.ord { toNat := a } { toNat := b } = (compare a b).then Ordering.eq

@[instance_reducible]

instance Aesop.instLTPremiseIndex : LT PremiseIndex

Equations

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

@[instance_reducible]

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

Equations

• Aesop.instDecidableRelPremiseIndexLt i j = i.toNat.decLt j.toNat

@[instance_reducible]

instance Aesop.instLEPremiseIndex : LE PremiseIndex

Equations

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

@[instance_reducible]

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

Equations

• Aesop.instDecidableRelPremiseIndexLe i j = i.toNat.decLe j.toNat

@[instance_reducible]

instance Aesop.instToStringPremiseIndex : ToString PremiseIndex

Equations

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