structure Aesop.LevelIndex : Type

• toNat : Nat

def Aesop.instInhabitedLevelIndex.default : LevelIndex

Equations

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

@[implicit_reducible]

instance Aesop.instInhabitedLevelIndex : Inhabited LevelIndex

Equations

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

@[implicit_reducible]

instance Aesop.instBEqLevelIndex : BEq LevelIndex

Equations

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

def Aesop.instBEqLevelIndex.beq : LevelIndex → LevelIndex → Bool

Equations

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

def Aesop.instHashableLevelIndex.hash : LevelIndex → UInt64

Equations

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

@[implicit_reducible]

instance Aesop.instHashableLevelIndex : Hashable LevelIndex

Equations

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

def Aesop.instDecidableEqLevelIndex.decEq (x✝ x✝¹ : LevelIndex) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableEqLevelIndex : DecidableEq LevelIndex

Equations

• Aesop.instDecidableEqLevelIndex = Aesop.instDecidableEqLevelIndex.decEq

def Aesop.instOrdLevelIndex.ord : LevelIndex → LevelIndex → Ordering

Equations

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

@[implicit_reducible]

instance Aesop.instOrdLevelIndex : Ord LevelIndex

Equations

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

@[implicit_reducible]

instance Aesop.instLTLevelIndex : LT LevelIndex

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableRelLevelIndexLt : DecidableRel fun (x1 x2 : LevelIndex) => x1 < x2

Equations

• Aesop.instDecidableRelLevelIndexLt i j = Aesop.instDecidableRelLevelIndexLt._aux_1 i j

@[implicit_reducible]

instance Aesop.instLELevelIndex : LE LevelIndex

Equations

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

@[implicit_reducible]

instance Aesop.instDecidableRelLevelIndexLe : DecidableRel fun (x1 x2 : LevelIndex) => x1 ≤ x2

Equations

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

@[implicit_reducible]

instance Aesop.instToStringLevelIndex : ToString LevelIndex

Equations

• Aesop.instToStringLevelIndex = { toString := fun (i : Aesop.LevelIndex) => toString i.toNat }