Documentation

Aesop.Forward.PremiseIndex

source
structure Aesop.PremiseIndex :
Type
Instances For
    source
    instance Aesop.instInhabitedPremiseIndex :
    Inhabited PremiseIndex
    Equations
      source
      instance Aesop.instBEqPremiseIndex :
      BEq PremiseIndex
      Equations
        source
        instance Aesop.instHashablePremiseIndex :
        Hashable PremiseIndex
        Equations
          source
          instance Aesop.instDecidableEqPremiseIndex :
          DecidableEq PremiseIndex
          Equations
            source
            instance Aesop.instOrdPremiseIndex :
            Ord PremiseIndex
            Equations
              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