Equations
- Aesop.instBEqSlotIndex = { beq := Aesop.beqSlotIndex✝ }
Equations
Equations
- Aesop.instOrdSlotIndex = { compare := Aesop.ordSlotIndex✝ }
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 }