structure Aesop.LevelIndex : Type

• toNat : Nat

instance Aesop.instInhabitedLevelIndex : Inhabited LevelIndex

Equations

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

instance Aesop.instBEqLevelIndex : BEq LevelIndex

Equations

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

instance Aesop.instHashableLevelIndex : Hashable LevelIndex

Equations

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

instance Aesop.instDecidableEqLevelIndex : DecidableEq LevelIndex

Equations

• Aesop.instDecidableEqLevelIndex = Aesop.decEqLevelIndex✝

instance Aesop.instOrdLevelIndex : Ord LevelIndex

Equations

• Aesop.instOrdLevelIndex = { compare := Aesop.ordLevelIndex✝ }

instance Aesop.instLTLevelIndex : LT LevelIndex

Equations

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

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

Equations

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

instance Aesop.instLELevelIndex : LE LevelIndex

Equations

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

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

Equations

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

instance Aesop.instToStringLevelIndex : ToString LevelIndex

Equations

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