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.

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

Computes m * 2^e.

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.

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

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

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.

instance instOfNatFloat {n : Nat} : OfNat Float 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.

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

Computes m * 2^e.

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.

instance instOfScientificFloat32 : OfScientific Float32

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

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.

instance instOfNatFloat32 {n : Nat} : OfNat Float32 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.