Documentation

Aesop.Forward.SlotIndex

source
structure Aesop.SlotIndex :
Type
Instances For
    source
    instance Aesop.instInhabitedSlotIndex :
    Inhabited SlotIndex
    Equations
      source
      instance Aesop.instBEqSlotIndex :
      BEq SlotIndex
      Equations
        source
        instance Aesop.instHashableSlotIndex :
        Hashable SlotIndex
        Equations
          source
          instance Aesop.instDecidableEqSlotIndex :
          DecidableEq SlotIndex
          Equations
            source
            instance Aesop.instOrdSlotIndex :
            Ord SlotIndex
            Equations
              source
              instance Aesop.instLTSlotIndex :
              LT SlotIndex
              Equations
                source
                instance Aesop.instDecidableRelSlotIndexLt :
                DecidableRel fun (x1 x2 : SlotIndex) => x1 < x2
                Equations
                  source
                  instance Aesop.instLESlotIndex :
                  LE SlotIndex
                  Equations
                    source
                    instance Aesop.instDecidableRelSlotIndexLe :
                    DecidableRel fun (x1 x2 : SlotIndex) => x1 ≤ x2
                    Equations
                      source
                      instance Aesop.instHAddSlotIndexNat :
                      HAdd SlotIndex Nat SlotIndex
                      Equations
                        source
                        instance Aesop.instHSubSlotIndexNat :
                        HSub SlotIndex Nat SlotIndex
                        Equations
                          source
                          instance Aesop.instToStringSlotIndex :
                          ToString SlotIndex
                          Equations