structure Aesop.SlotIndex : Type

• toNat : Nat

@[implicit_reducible]

instance Aesop.instInhabitedSlotIndex : Inhabited SlotIndex

Equations

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

def Aesop.instInhabitedSlotIndex.default : SlotIndex

Equations

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

@[implicit_reducible]

instance Aesop.instBEqSlotIndex : BEq SlotIndex

Equations

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

def Aesop.instBEqSlotIndex.beq : SlotIndex → SlotIndex → Bool

Equations

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

@[implicit_reducible]

instance Aesop.instHashableSlotIndex : Hashable SlotIndex

Equations

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

def Aesop.instHashableSlotIndex.hash : SlotIndex → UInt64

Equations

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

def Aesop.instDecidableEqSlotIndex.decEq (x✝ x✝¹ : SlotIndex) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableEqSlotIndex : DecidableEq SlotIndex

Equations

• Aesop.instDecidableEqSlotIndex = Aesop.instDecidableEqSlotIndex.decEq

@[implicit_reducible]

instance Aesop.instOrdSlotIndex : Ord SlotIndex

Equations

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

def Aesop.instOrdSlotIndex.ord : SlotIndex → SlotIndex → Ordering

Equations

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

@[implicit_reducible]

instance Aesop.instLTSlotIndex : LT SlotIndex

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableRelSlotIndexLt : DecidableRel fun (x1 x2 : SlotIndex) => x1 < x2

Equations

• Aesop.instDecidableRelSlotIndexLt i j = Aesop.instDecidableRelSlotIndexLt._aux_1 i j

@[implicit_reducible]

instance Aesop.instLESlotIndex : LE SlotIndex

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableRelSlotIndexLe : DecidableRel fun (x1 x2 : SlotIndex) => x1 ≤ x2

Equations

• Aesop.instDecidableRelSlotIndexLe i j = if h : i.toNat.ble j.toNat = true then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aesop.instHAddSlotIndexNat : HAdd SlotIndex Nat SlotIndex

Equations

• Aesop.instHAddSlotIndexNat = { hAdd := fun (i : Aesop.SlotIndex) (j : Nat) => { toNat := i.toNat + j } }

@[implicit_reducible]

instance Aesop.instHSubSlotIndexNat : HSub SlotIndex Nat SlotIndex

Equations

• Aesop.instHSubSlotIndexNat = { hSub := fun (i : Aesop.SlotIndex) (j : Nat) => { toNat := i.toNat - j } }

@[implicit_reducible]

instance Aesop.instToStringSlotIndex : ToString SlotIndex

Equations

• Aesop.instToStringSlotIndex = { toString := fun (i : Aesop.SlotIndex) => toString i.toNat }