Documentation

Init.Data.Float

structure FloatSpec :
Instances For
    structure Float :

    Native floating point type, corresponding to the IEEE 754 binary64 format (double in C or f64 in Rust).

    Instances For
      Equations
      @[extern lean_float_add]
      opaque Float.add :
      FloatFloatFloat
      @[extern lean_float_sub]
      opaque Float.sub :
      FloatFloatFloat
      @[extern lean_float_mul]
      opaque Float.mul :
      FloatFloatFloat
      @[extern lean_float_div]
      opaque Float.div :
      FloatFloatFloat
      @[extern lean_float_negate]
      opaque Float.neg :
      def Float.lt :
      FloatFloatProp
      Equations
      • a.lt b = match a, b with | { val := a }, { val := b } => floatSpec.lt a b
      Instances For
        def Float.le :
        FloatFloatProp
        Equations
        Instances For
          Equations
          Equations
          Equations
          Equations
          Equations
          instance instLTFloat :
          Equations
          instance instLEFloat :
          Equations
          @[extern lean_float_beq]
          opaque Float.beq (a : Float) (b : Float) :

          Note: this is not reflexive since NaN != NaN.

          Equations
          @[extern lean_float_decLt]
          opaque Float.decLt (a : Float) (b : Float) :
          Decidable (a < b)
          @[extern lean_float_decLe]
          opaque Float.decLe (a : Float) (b : Float) :
          instance floatDecLt (a : Float) (b : Float) :
          Decidable (a < b)
          Equations
          instance floatDecLe (a : Float) (b : Float) :
          Equations
          @[extern lean_float_to_string]
          @[extern lean_float_to_uint8]

          If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt8 (including Inf), returns the maximum value of UInt8 (i.e. UInt8.size - 1).

          @[extern lean_float_to_uint16]

          If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt16 (including Inf), returns the maximum value of UInt16 (i.e. UInt16.size - 1).

          @[extern lean_float_to_uint32]

          If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt32 (including Inf), returns the maximum value of UInt32 (i.e. UInt32.size - 1).

          @[extern lean_float_to_uint64]

          If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt64 (including Inf), returns the maximum value of UInt64 (i.e. UInt64.size - 1).

          @[extern lean_float_to_usize]

          If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for USize (including Inf), returns the maximum value of USize (i.e. USize.size - 1). This value is platform dependent).

          @[extern lean_float_isnan]
          opaque Float.isNaN :
          @[extern lean_float_isfinite]
          @[extern lean_float_isinf]
          opaque Float.isInf :
          @[extern lean_float_frexp]

          Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s ∈ (-1;-0.5] ∪ [0.5; 1). Returns an undefined value if x is not finite.

          @[extern lean_uint64_to_float]
          Equations
          @[extern sin]
          opaque Float.sin :
          @[extern cos]
          opaque Float.cos :
          @[extern tan]
          opaque Float.tan :
          @[extern asin]
          opaque Float.asin :
          @[extern acos]
          opaque Float.acos :
          @[extern atan]
          opaque Float.atan :
          @[extern atan2]
          opaque Float.atan2 :
          FloatFloatFloat
          @[extern sinh]
          opaque Float.sinh :
          @[extern cosh]
          opaque Float.cosh :
          @[extern tanh]
          opaque Float.tanh :
          @[extern asinh]
          opaque Float.asinh :
          @[extern acosh]
          opaque Float.acosh :
          @[extern atanh]
          opaque Float.atanh :
          @[extern exp]
          opaque Float.exp :
          @[extern exp2]
          opaque Float.exp2 :
          @[extern log]
          opaque Float.log :
          @[extern log2]
          opaque Float.log2 :
          @[extern log10]
          opaque Float.log10 :
          @[extern pow]
          opaque Float.pow :
          FloatFloatFloat
          @[extern sqrt]
          opaque Float.sqrt :
          @[extern cbrt]
          opaque Float.cbrt :
          @[extern ceil]
          opaque Float.ceil :
          @[extern floor]
          opaque Float.floor :
          @[extern round]
          opaque Float.round :
          @[extern fabs]
          opaque Float.abs :
          Equations
          Equations
          @[extern lean_float_scaleb]
          opaque Float.scaleB (x : Float) (i : Int) :

          Efficiently computes x * 2^i.