Documentation

Aesop.Forward.SlotIndex

structure Aesop.SlotIndex :

toNat : Nat

instance Aesop.instInhabitedSlotIndex :

Inhabited SlotIndex

Equations

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

instance Aesop.instBEqSlotIndex :

Equations

Aesop.instBEqSlotIndex = { beq := Aesop.beqSlotIndex✝ }

instance Aesop.instHashableSlotIndex :

Hashable SlotIndex

Equations

Aesop.instHashableSlotIndex = { hash := Aesop.hashSlotIndex✝ }

instance Aesop.instDecidableEqSlotIndex :

DecidableEq SlotIndex

Equations

Aesop.instDecidableEqSlotIndex = Aesop.decEqSlotIndex✝

instance Aesop.instOrdSlotIndex :

Equations

Aesop.instOrdSlotIndex = { compare := Aesop.ordSlotIndex✝ }

instance Aesop.instLTSlotIndex :

Equations

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

instance Aesop.instDecidableRelSlotIndexLt :

DecidableRel fun (x1 x2 : SlotIndex) => x1 < x2

Equations

Aesop.instDecidableRelSlotIndexLt i j = inferInstanceAs (Decidable (i.toNat < j.toNat))

instance Aesop.instLESlotIndex :

Equations

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

instance Aesop.instDecidableRelSlotIndexLe :

DecidableRel fun (x1 x2 : SlotIndex) => x1 ≤ x2

Equations

Aesop.instDecidableRelSlotIndexLe i j = inferInstanceAs (Decidable (i.toNat ≤ j.toNat))

instance Aesop.instHAddSlotIndexNat :

HAdd SlotIndex Nat SlotIndex

Equations

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

instance Aesop.instHSubSlotIndexNat :

HSub SlotIndex Nat SlotIndex

Equations

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

instance Aesop.instToStringSlotIndex :

ToString SlotIndex

Equations

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