Documentation

Aesop.Forward.PremiseIndex

source
structure Aesop.PremiseIndex :
Type
Instances For
    source
    @[implicit_reducible]
    instance Aesop.instInhabitedPremiseIndex :
    Inhabited PremiseIndex
    source
    def Aesop.instInhabitedPremiseIndex.default :
    PremiseIndex
    Instances For
      source
      @[implicit_reducible]
      instance Aesop.instBEqPremiseIndex :
      BEq PremiseIndex
      source
      def Aesop.instBEqPremiseIndex.beq :
      PremiseIndex → PremiseIndex → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Aesop.instHashablePremiseIndex :
        Hashable PremiseIndex
        source
        def Aesop.instHashablePremiseIndex.hash :
        PremiseIndex → UInt64
        Instances For
          source
          def Aesop.instDecidableEqPremiseIndex.decEq (x✝ x✝¹ : PremiseIndex) :
          Decidable (x✝ = x✝¹)
          Instances For
            source
            @[implicit_reducible]
            instance Aesop.instDecidableEqPremiseIndex :
            DecidableEq PremiseIndex
            source
            @[implicit_reducible]
            instance Aesop.instOrdPremiseIndex :
            Ord PremiseIndex
            source
            def Aesop.instOrdPremiseIndex.ord :
            PremiseIndex → PremiseIndex → Ordering
            Instances For
              source
              @[implicit_reducible]
              instance Aesop.instLTPremiseIndex :
              LT PremiseIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelPremiseIndexLt :
              DecidableRel fun (x1 x2 : PremiseIndex) => x1 < x2
              source
              @[implicit_reducible]
              instance Aesop.instLEPremiseIndex :
              LE PremiseIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelPremiseIndexLe :
              DecidableRel fun (x1 x2 : PremiseIndex) => x1 ≤ x2
              source
              @[implicit_reducible]
              instance Aesop.instToStringPremiseIndex :
              ToString PremiseIndex