Documentation

Aesop.Forward.SlotIndex

source
structure Aesop.SlotIndex :
Type
Instances For
    source
    def Aesop.instInhabitedSlotIndex.default :
    SlotIndex
    Equations
      Instances For
        source
        instance Aesop.instInhabitedSlotIndex :
        Inhabited SlotIndex
        Equations
          source
          def Aesop.instBEqSlotIndex.beq :
          SlotIndex → SlotIndex → Bool
          Equations
            Instances For
              source
              instance Aesop.instBEqSlotIndex :
              BEq SlotIndex
              Equations
                source
                instance Aesop.instHashableSlotIndex :
                Hashable SlotIndex
                Equations
                  source
                  def Aesop.instHashableSlotIndex.hash :
                  SlotIndex → UInt64
                  Equations
                    Instances For
                      source
                      instance Aesop.instDecidableEqSlotIndex :
                      DecidableEq SlotIndex
                      Equations
                        source
                        def Aesop.instDecidableEqSlotIndex.decEq (x✝ x✝¹ : SlotIndex) :
                        Decidable (x✝ = x✝¹)
                        Equations
                          Instances For
                            source
                            def Aesop.instOrdSlotIndex.ord :
                            SlotIndex → SlotIndex → Ordering
                            Equations
                              Instances For
                                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