Documentation

Aesop.Forward.LevelIndex

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