Documentation

Aesop.Forward.PremiseIndex

source
structure Aesop.PremiseIndex :
Type
Instances For
    source
    @[instance_reducible]
    instance Aesop.instInhabitedPremiseIndex :
    Inhabited PremiseIndex
    source
    @[instance_reducible]
    instance Aesop.instBEqPremiseIndex :
    BEq PremiseIndex
    source
    def Aesop.instBEqPremiseIndex.beq :
    PremiseIndex → PremiseIndex → Bool
    Instances For
      source
      @[instance_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
          @[instance_reducible]
          instance Aesop.instDecidableEqPremiseIndex :
          DecidableEq PremiseIndex
          source
          @[instance_reducible]
          instance Aesop.instOrdPremiseIndex :
          Ord PremiseIndex
          source
          def Aesop.instOrdPremiseIndex.ord :
          PremiseIndex → PremiseIndex → Ordering
          Instances For
            source
            @[instance_reducible]
            instance Aesop.instLTPremiseIndex :
            LT PremiseIndex
            source
            @[instance_reducible]
            instance Aesop.instDecidableRelPremiseIndexLt :
            DecidableRel fun (x1 x2 : PremiseIndex) => x1 < x2
            source
            @[instance_reducible]
            instance Aesop.instLEPremiseIndex :
            LE PremiseIndex
            source
            @[instance_reducible]
            instance Aesop.instDecidableRelPremiseIndexLe :
            DecidableRel fun (x1 x2 : PremiseIndex) => x1 ≤ x2
            source
            @[instance_reducible]
            instance Aesop.instToStringPremiseIndex :
            ToString PremiseIndex