Documentation

Aesop.Forward.LevelIndex

source
structure Aesop.LevelIndex :
Type
Instances For
    source
    instance Aesop.instInhabitedLevelIndex :
    Inhabited LevelIndex
    Equations
      source
      instance Aesop.instBEqLevelIndex :
      BEq LevelIndex
      Equations
        source
        instance Aesop.instHashableLevelIndex :
        Hashable LevelIndex
        Equations
          source
          instance Aesop.instDecidableEqLevelIndex :
          DecidableEq LevelIndex
          Equations
            source
            instance Aesop.instOrdLevelIndex :
            Ord LevelIndex
            Equations
              source
              instance Aesop.instLTLevelIndex :
              LT LevelIndex
              Equations
                source
                instance Aesop.instDecidableRelLevelIndexLt :
                DecidableRel fun (x1 x2 : LevelIndex) => x1 < x2
                Equations
                  source
                  instance Aesop.instLELevelIndex :
                  LE LevelIndex
                  Equations
                    source
                    instance Aesop.instDecidableRelLevelIndexLe :
                    DecidableRel fun (x1 x2 : LevelIndex) => x1 ≤ x2
                    Equations
                      source
                      instance Aesop.instToStringLevelIndex :
                      ToString LevelIndex
                      Equations