source
class OfScientific (α : Type u) :
Type u

For decimal and scientific numbers (e.g., `1.23`, `3.12e10`). Examples:

- `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
- `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`

Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.

- ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : α

  Produces a value from the given mantissa, exponent sign, and decimal exponent. For the exponent sign, `true` indicates a negative exponent.

  Examples:

  - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
  - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`

  Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.

Instances

source
def Float.ofBinaryScientific (m : Nat) (e : Int) :
Float

Computes `m * 2^e`.

Equations

- Float.ofBinaryScientific m e = (m >>> (m.log2 - 63)).toUInt64.toFloat.scaleB (e + ↑(m.log2 - 63))

Instances For

source
opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) :
Float

Constructs a `Float` from the given mantissa, sign, and exponent values.

This function is part of the implementation of the `OfScientific Float` instance that is used to interpret floating-point literals.

source
@[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 }

source
@[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

Instances For

source
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

Instances For

source
instance instOfNatFloat {n : Nat} :
OfNat Float n
Equations

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

source
@[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

Instances For

source
def Float32.ofBinaryScientific (m : Nat) (e : Int) :
Float32

Computes `m * 2^e`.

Equations

- Float32.ofBinaryScientific m e = (m >>> (m.log2 - 63)).toUInt64.toFloat32.scaleB (e + ↑(m.log2 - 63))

Instances For

source
opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) :
Float32

Constructs a `Float32` from the given mantissa, sign, and exponent values.

This function is part of the implementation of the `OfScientific Float32` instance that is used to interpret floating-point literals.

source
instance instOfScientificFloat32 :
OfScientific Float32
Equations

- instOfScientificFloat32 = { ofScientific := Float32.ofScientific }

source
@[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

Instances For

source
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

Instances For

source
instance instOfNatFloat32 {n : Nat} :
OfNat Float32 n
Equations

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

source
@[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

Instances For