def Float.exactlyRepresentablePowersOfTen : Array Float

Precomputed values of 10 ^ e for 0 ≤ e ≤ 22. In this range, the values can be represented exactly.

Equations

• One or more equations did not get rendered due to their size.

def Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, defaultInstance 501]

instance instOfScientificFloat : OfScientific Float

The OfScientific Float must have priority higher than mid since the default instance Neg Int has mid priority.

#check -42.0 -- must be Float

Equations

• instOfScientificFloat = { ofScientific := Float.ofScientific }

@[export lean_float_of_nat]

def Float.ofNat (n : Nat) : Float

Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite floating-point value if the range of Float is exceeded.

Equations

• Float.ofNat n = OfScientific.ofScientific n false 0

def Float.ofInt : Int → Float

Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative infinite floating-point value if the range of Float is exceeded.

Equations

• Float.ofInt (Int.ofNat n) = Float.ofNat n
• Float.ofInt (Int.negSucc n) = (Float.ofNat n.succ).neg

@[instance_reducible]

instance instOfNatFloat {n : Nat} : OfNat Float n

Equations

• instOfNatFloat = { ofNat := Float.ofNat n }

@[reducible, inline]

abbrev Nat.toFloat (n : Nat) : Float

Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite floating-point value if the range of Float is exceeded.

Equations

• n.toFloat = Float.ofNat n

@[reducible, inline]

abbrev Int.toFloat (n : Int) : Float

Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative infinite floating-point value if the range of Float is exceeded.

Equations

• n.toFloat = Float.ofInt n

def Float32.exactlyRepresentablePowersOfTen : Array Float32

Precomputed values of 10 ^ e for 0 ≤ e ≤ 10 . In this range, the values can be represented exactly.

Equations

• One or more equations did not get rendered due to their size.

def Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instOfScientificFloat32 : OfScientific Float32

Equations

• instOfScientificFloat32 = { ofScientific := Float32.ofScientific }

@[export lean_float32_of_nat]

def Float32.ofNat (n : Nat) : Float32

Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite floating-point value if the range of Float32 is exceeded.

Equations

• Float32.ofNat n = OfScientific.ofScientific n false 0

def Float32.ofInt : Int → Float32

Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative infinite floating-point value if the range of Float32 is exceeded.

Equations

• Float32.ofInt (Int.ofNat n) = Float32.ofNat n
• Float32.ofInt (Int.negSucc n) = (Float32.ofNat n.succ).neg

@[instance_reducible]

instance instOfNatFloat32 {n : Nat} : OfNat Float32 n

Equations

• instOfNatFloat32 = { ofNat := Float32.ofNat n }

@[reducible, inline]

abbrev Nat.toFloat32 (n : Nat) : Float32

Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite floating-point value if the range of Float32 is exceeded.

Equations

• n.toFloat32 = Float32.ofNat n

@[reducible, inline]

abbrev Int.toFloat32 (n : Int) : Float32

Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative infinite floating-point value if the range of Float32 is exceeded.

Equations

• n.toFloat32 = Float32.ofInt n