Documentation

Aesop.Forward.LevelIndex

source
structure Aesop.LevelIndex :
Type
Instances For
    source
    @[implicit_reducible]
    instance Aesop.instInhabitedLevelIndex :
    Inhabited LevelIndex
    source
    def Aesop.instInhabitedLevelIndex.default :
    LevelIndex
    Instances For
      source
      def Aesop.instBEqLevelIndex.beq :
      LevelIndex → LevelIndex → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Aesop.instBEqLevelIndex :
        BEq LevelIndex
        source
        def Aesop.instHashableLevelIndex.hash :
        LevelIndex → UInt64
        Instances For
          source
          @[implicit_reducible]
          instance Aesop.instHashableLevelIndex :
          Hashable LevelIndex
          source
          def Aesop.instDecidableEqLevelIndex.decEq (x✝ x✝¹ : LevelIndex) :
          Decidable (x✝ = x✝¹)
          Instances For
            source
            @[implicit_reducible]
            instance Aesop.instDecidableEqLevelIndex :
            DecidableEq LevelIndex
            source
            @[implicit_reducible]
            instance Aesop.instOrdLevelIndex :
            Ord LevelIndex
            source
            def Aesop.instOrdLevelIndex.ord :
            LevelIndex → LevelIndex → Ordering
            Instances For
              source
              @[implicit_reducible]
              instance Aesop.instLTLevelIndex :
              LT LevelIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelLevelIndexLt :
              DecidableRel fun (x1 x2 : LevelIndex) => x1 < x2
              source
              @[implicit_reducible]
              instance Aesop.instLELevelIndex :
              LE LevelIndex
              source
              @[implicit_reducible]
              instance Aesop.instDecidableRelLevelIndexLe :
              DecidableRel fun (x1 x2 : LevelIndex) => x1 ≤ x2
              source
              @[implicit_reducible]
              instance Aesop.instToStringLevelIndex :
              ToString LevelIndex