Documentation

Aesop.Percent

source
structure Aesop.Percent :
Type
Instances For
    source
    @[implicit_reducible]
    instance Aesop.instInhabitedPercent :
    Inhabited Percent
    source
    def Aesop.instInhabitedPercent.default :
    Percent
    Instances For
      source
      def Aesop.Percent.ofFloat (f : Float) :
      Option Percent
      Instances For
        source
        @[implicit_reducible]
        instance Aesop.Percent.instMul :
        Mul Percent
        source
        @[inline]
        def Aesop.Percent.δ :
        Percent
        Instances For
          source
          @[implicit_reducible]
          instance Aesop.Percent.instBEq :
          BEq Percent
          source
          @[implicit_reducible]
          instance Aesop.Percent.instOrd :
          Ord Percent
          source
          @[implicit_reducible]
          instance Aesop.Percent.instLT :
          LT Percent
          source
          @[implicit_reducible]
          instance Aesop.Percent.instLE :
          LE Percent
          source
          @[implicit_reducible]
          instance Aesop.Percent.instToString :
          ToString Percent
          source
          @[implicit_reducible]
          instance Aesop.Percent.instHPowNat :
          HPow Percent Nat Percent
          source
          def Aesop.Percent.hundred :
          Percent
          Instances For
            source
            def Aesop.Percent.fifty :
            Percent
            Instances For
              source
              def Aesop.Percent.toHumanString (p : Percent) :
              String
              Instances For
                source
                def Aesop.Percent.ofNat (n : Nat) :
                Option Percent
                Instances For