Documentation

Aesop.Forward.SlotIndex

source
structure Aesop.SlotIndex :
Type
Instances For
    source
    def Aesop.instInhabitedSlotIndex.default :
    SlotIndex
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.instInhabitedSlotIndex :
      Inhabited SlotIndex
      source
      def Aesop.instBEqSlotIndex.beq :
      SlotIndex → SlotIndex → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Aesop.instBEqSlotIndex :
        BEq SlotIndex
        source
        @[implicit_reducible]
        instance Aesop.instHashableSlotIndex :
        Hashable SlotIndex
        source
        def Aesop.instHashableSlotIndex.hash :
        SlotIndex → UInt64
        Instances For
          source
          @[implicit_reducible]
          instance Aesop.instDecidableEqSlotIndex :
          DecidableEq SlotIndex
          source
          def Aesop.instDecidableEqSlotIndex.decEq (x✝ x✝¹ : SlotIndex) :
          Decidable (x✝ = x✝¹)
          Instances For
            source
            def Aesop.instOrdSlotIndex.ord :
            SlotIndex → SlotIndex → Ordering
            Instances For
              source
              @[implicit_reducible]
              instance Aesop.instOrdSlotIndex :
              Ord SlotIndex
              source
              @[implicit_reducible]
              instance Aesop.instLTSlotIndex :
              LT SlotIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelSlotIndexLt :
              DecidableRel fun (x1 x2 : SlotIndex) => x1 < x2
              source
              @[implicit_reducible]
              instance Aesop.instLESlotIndex :
              LE SlotIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelSlotIndexLe :
              DecidableRel fun (x1 x2 : SlotIndex) => x1 ≤ x2
              source
              @[implicit_reducible]
              instance Aesop.instHAddSlotIndexNat :
              HAdd SlotIndex Nat SlotIndex
              source
              @[implicit_reducible]
              instance Aesop.instHSubSlotIndexNat :
              HSub SlotIndex Nat SlotIndex
              source
              @[implicit_reducible]
              instance Aesop.instToStringSlotIndex :
              ToString SlotIndex