Documentation

Aesop.Forward.LevelIndex

structure Aesop.LevelIndex :

toNat : Nat

Instances For

instance Aesop.instInhabitedLevelIndex :

Inhabited LevelIndex

Equations

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

instance Aesop.instBEqLevelIndex :

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 :

Equations

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

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 }