Documentation

Aesop.Forward.PremiseIndex

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