Documentation

Aesop.Forward.SlotIndex

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