Equations
- Aesop.instInhabitedSlotIndex.default = { toNat := default }
Instances For
Equations
Equations
- Aesop.instBEqSlotIndex.beq { toNat := a } { toNat := b } = (a == b)
- Aesop.instBEqSlotIndex.beq x✝¹ x✝ = false
Instances For
Equations
Equations
Instances For
Equations
- Aesop.instOrdSlotIndex.ord { toNat := a } { toNat := b } = (compare a b).then Ordering.eq
Instances For
Equations
- Aesop.instOrdSlotIndex = { compare := Aesop.instOrdSlotIndex.ord }
Equations
- Aesop.instLTSlotIndex = { lt := fun (i j : Aesop.SlotIndex) => i.toNat < j.toNat }
Equations
- Aesop.instDecidableRelSlotIndexLt i j = inferInstanceAs (Decidable (i.toNat < j.toNat))
Equations
- Aesop.instLESlotIndex = { le := fun (i j : Aesop.SlotIndex) => i.toNat ≤ j.toNat }
Equations
- Aesop.instDecidableRelSlotIndexLe i j = inferInstanceAs (Decidable (i.toNat ≤ j.toNat))
Equations
- Aesop.instToStringSlotIndex = { toString := fun (i : Aesop.SlotIndex) => toString i.toNat }