Documentation

Aesop.Percent

source
structure Aesop.Percent :
Type
Instances For
    source
    @[instance_reducible]
    instance Aesop.instInhabitedPercent :
    Inhabited Percent
    source
    def Aesop.Percent.ofFloat (f : Float) :
    Option Percent
    Instances For
      source
      @[instance_reducible]
      instance Aesop.Percent.instMul :
      Mul Percent
      source
      @[inline]
      def Aesop.Percent.δ :
      Percent
      Instances For
        source
        @[instance_reducible]
        instance Aesop.Percent.instBEq :
        BEq Percent
        source
        @[instance_reducible]
        instance Aesop.Percent.instOrd :
        Ord Percent
        source
        @[instance_reducible]
        instance Aesop.Percent.instLT :
        LT Percent
        source
        @[instance_reducible]
        instance Aesop.Percent.instLE :
        LE Percent
        source
        @[instance_reducible]
        instance Aesop.Percent.instToString :
        ToString Percent
        source
        @[instance_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