Documentation

Aesop.Forward.LevelIndex

source
structure Aesop.LevelIndex :
Type
Instances For
    source
    instance Aesop.instInhabitedLevelIndex :
    Inhabited LevelIndex
    Equations
      source
      def Aesop.instInhabitedLevelIndex.default :
      LevelIndex
      Equations
        Instances For
          source
          def Aesop.instBEqLevelIndex.beq :
          LevelIndex → LevelIndex → Bool
          Equations
            Instances For
              source
              instance Aesop.instBEqLevelIndex :
              BEq LevelIndex
              Equations
                source
                def Aesop.instHashableLevelIndex.hash :
                LevelIndex → UInt64
                Equations
                  Instances For
                    source
                    instance Aesop.instHashableLevelIndex :
                    Hashable LevelIndex
                    Equations
                      source
                      def Aesop.instDecidableEqLevelIndex.decEq (x✝ x✝¹ : LevelIndex) :
                      Decidable (x✝ = x✝¹)
                      Equations
                        Instances For
                          source
                          instance Aesop.instDecidableEqLevelIndex :
                          DecidableEq LevelIndex
                          Equations
                            source
                            instance Aesop.instOrdLevelIndex :
                            Ord LevelIndex
                            Equations
                              source
                              def Aesop.instOrdLevelIndex.ord :
                              LevelIndex → LevelIndex → Ordering
                              Equations
                                Instances For
                                  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