Documentation

Init.Data.Float.Model.Unpacked.Operations.OfNat

source
def Float.Model.UnpackedFloat.ofInt (spec : Format) (n : Int) :
UnpackedFloat

Converts an Int to an UnpackedFloat, returning positive zero on zero.

Equations
Instances For
    source
    def Float.Model.UnpackedFloat.ofNat (spec : Format) (n : Nat) :
    UnpackedFloat

    Converts a Nat to an UnpackedFloat, returning positive zero on zero.

    Equations
    Instances For
      source
      def Float.Model.UnpackedFloat.ofUInt8 (spec : Format) (n : UInt8) :
      UnpackedFloat

      Converts a UInt8 to an UnpackedFloat, returning positive zero on zero.

      Equations
      Instances For
        source
        def Float.Model.UnpackedFloat.ofUInt16 (spec : Format) (n : UInt16) :
        UnpackedFloat

        Converts a UInt16 to an UnpackedFloat, returning positive zero on zero.

        Equations
        Instances For
          source
          def Float.Model.UnpackedFloat.ofUInt32 (spec : Format) (n : UInt32) :
          UnpackedFloat

          Converts a UInt32 to an UnpackedFloat, returning positive zero on zero.

          Equations
          Instances For
            source
            def Float.Model.UnpackedFloat.ofUInt64 (spec : Format) (n : UInt64) :
            UnpackedFloat

            Converts a UInt64 to an UnpackedFloat, returning positive zero on zero.

            Equations
            Instances For
              source
              def Float.Model.UnpackedFloat.ofUSize (spec : Format) (n : USize) :
              UnpackedFloat

              Converts a USize to an UnpackedFloat, returning positive zero on zero.

              Equations
              Instances For
                source
                def Float.Model.UnpackedFloat.ofInt8 (spec : Format) (n : Int8) :
                UnpackedFloat

                Converts an Int8 to an UnpackedFloat, returning positive zero on zero.

                Equations
                Instances For
                  source
                  def Float.Model.UnpackedFloat.ofInt16 (spec : Format) (n : Int16) :
                  UnpackedFloat

                  Converts an Int16 to an UnpackedFloat, returning positive zero on zero.

                  Equations
                  Instances For
                    source
                    def Float.Model.UnpackedFloat.ofInt32 (spec : Format) (n : Int32) :
                    UnpackedFloat

                    Converts an Int32 to an UnpackedFloat, returning positive zero on zero.

                    Equations
                    Instances For
                      source
                      def Float.Model.UnpackedFloat.ofInt64 (spec : Format) (n : Int64) :
                      UnpackedFloat

                      Converts an Int64 to an UnpackedFloat, returning positive zero on zero.

                      Equations
                      Instances For
                        source
                        def Float.Model.UnpackedFloat.ofISize (spec : Format) (n : ISize) :
                        UnpackedFloat

                        Converts an ISize to an UnpackedFloat, returning positive zero on zero.

                        Equations
                        Instances For