Documentation

Aesop.Forward.LevelIndex

structure Aesop.LevelIndex :

toNat : Nat

Instances For

instance Aesop.instInhabitedLevelIndex :

Inhabited LevelIndex

Equations

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

def Aesop.instInhabitedLevelIndex.default :

Equations

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

Instances For

def Aesop.instBEqLevelIndex.beq :

LevelIndex → LevelIndex → Bool

Equations

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

Instances For

instance Aesop.instBEqLevelIndex :

Equations

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

def Aesop.instHashableLevelIndex.hash :

LevelIndex → UInt64

Equations

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

Instances For

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 ⋯

Instances For

instance Aesop.instDecidableEqLevelIndex :

DecidableEq LevelIndex

Equations

Aesop.instDecidableEqLevelIndex = Aesop.instDecidableEqLevelIndex.decEq

instance Aesop.instOrdLevelIndex :

Equations

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

def Aesop.instOrdLevelIndex.ord :

LevelIndex → LevelIndex → Ordering

Equations

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

Instances For

instance Aesop.instLTLevelIndex :

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 :

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 }