structure FloatSpec : Type 1

• float : Type
• val : self.float
• lt : self.float → self.float → Prop
• le : self.float → self.float → Prop
• decLt : DecidableRel self.lt
• decLe : DecidableRel self.le

opaque floatSpec : FloatSpec

structure Float : Type

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

• val : floatSpec.float

instance instInhabitedFloat : Inhabited Float

Equations

• instInhabitedFloat = { default := { val := floatSpec.val } }

@[extern lean_float_add]

opaque Float.add : Float → Float → Float

@[extern lean_float_sub]

opaque Float.sub : Float → Float → Float

@[extern lean_float_mul]

opaque Float.mul : Float → Float → Float

@[extern lean_float_div]

opaque Float.div : Float → Float → Float

@[extern lean_float_negate]

opaque Float.neg : Float → Float

def Float.lt : Float → Float → Prop

Equations

• a.lt b = match a, b with | { val := a }, { val := b } => floatSpec.lt a b

def Float.le : Float → Float → Prop

Equations

• a.le b = floatSpec.le a.val b.val

instance instAddFloat : Add Float

Equations

• instAddFloat = { add := Float.add }

instance instSubFloat : Sub Float

Equations

• instSubFloat = { sub := Float.sub }

instance instMulFloat : Mul Float

Equations

• instMulFloat = { mul := Float.mul }

instance instDivFloat : Div Float

Equations

• instDivFloat = { div := Float.div }

instance instNegFloat : Neg Float

Equations

• instNegFloat = { neg := Float.neg }

instance instLTFloat : LT Float

Equations

• instLTFloat = { lt := Float.lt }

instance instLEFloat : LE Float

Equations

• instLEFloat = { le := Float.le }

@[extern lean_float_beq]

opaque Float.beq (a b : Float) : Bool

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

instance instBEqFloat : BEq Float

Equations

• instBEqFloat = { beq := Float.beq }

@[extern lean_float_decLt]

opaque Float.decLt (a b : Float) : Decidable (a < b)

@[extern lean_float_decLe]

opaque Float.decLe (a b : Float) : Decidable (a ≤ b)

instance floatDecLt (a b : Float) : Decidable (a < b)

Equations

• floatDecLt a b = a.decLt b

instance floatDecLe (a b : Float) : Decidable (a ≤ b)

Equations

• floatDecLe a b = a.decLe b

@[extern lean_float_to_string]

opaque Float.toString : Float → String

@[extern lean_float_to_uint8]

opaque Float.toUInt8 : Float → 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]

opaque Float.toUInt16 : Float → 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]

opaque Float.toUInt32 : Float → 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]

opaque Float.toUInt64 : Float → 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]

opaque Float.toUSize : Float → 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 : Float → Bool

@[extern lean_float_isfinite]

opaque Float.isFinite : Float → Bool

@[extern lean_float_isinf]

opaque Float.isInf : Float → Bool

@[extern lean_float_frexp]

opaque Float.frExp : Float → Float × Int

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.

instance instToStringFloat : ToString Float

Equations

• instToStringFloat = { toString := Float.toString }

@[extern lean_uint64_to_float]

opaque UInt64.toFloat (n : UInt64) : Float

instance instReprFloat : Repr Float

Equations

• instReprFloat = { reprPrec := fun (n : Float) (prec : Nat) => if n < UInt64.toFloat 0 then Repr.addAppParen (Std.Format.text (toString n)) prec else Std.Format.text (toString n) }

instance instReprAtomFloat : ReprAtom Float

Equations

• instReprAtomFloat = { }

@[extern sin]

opaque Float.sin : Float → Float

@[extern cos]

opaque Float.cos : Float → Float

@[extern tan]

opaque Float.tan : Float → Float

@[extern asin]

opaque Float.asin : Float → Float

@[extern acos]

opaque Float.acos : Float → Float

@[extern atan]

opaque Float.atan : Float → Float

@[extern atan2]

opaque Float.atan2 : Float → Float → Float

@[extern sinh]

opaque Float.sinh : Float → Float

@[extern cosh]

opaque Float.cosh : Float → Float

@[extern tanh]

opaque Float.tanh : Float → Float

@[extern asinh]

opaque Float.asinh : Float → Float

@[extern acosh]

opaque Float.acosh : Float → Float

@[extern atanh]

opaque Float.atanh : Float → Float

@[extern exp]

opaque Float.exp : Float → Float

@[extern exp2]

opaque Float.exp2 : Float → Float

@[extern log]

opaque Float.log : Float → Float

@[extern log2]

opaque Float.log2 : Float → Float

@[extern log10]

opaque Float.log10 : Float → Float

@[extern pow]

opaque Float.pow : Float → Float → Float

@[extern sqrt]

opaque Float.sqrt : Float → Float

@[extern cbrt]

opaque Float.cbrt : Float → Float

@[extern ceil]

opaque Float.ceil : Float → Float

@[extern floor]

opaque Float.floor : Float → Float

@[extern round]

opaque Float.round : Float → Float

@[extern fabs]

opaque Float.abs : Float → Float

instance instHomogeneousPowFloat : HomogeneousPow Float

Equations

• instHomogeneousPowFloat = { pow := Float.pow }

instance instMinFloat : Min Float

Equations

• instMinFloat = minOfLe

instance instMaxFloat : Max Float

Equations

• instMaxFloat = maxOfLe

@[extern lean_float_scaleb]

opaque Float.scaleB (x : Float) (i : Int) : Float

Efficiently computes x * 2^i.