class OfScientific (α : Type u) : Type u

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

• OfScientific.ofScientific 123 true 2 represents 1.23
• OfScientific.ofScientific 121 false 100 represents 121e100

• ofScientific : Nat → Bool → Nat → α

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

Computes m * 2^e.

Equations

• Float.ofBinaryScientific m e = let s := Nat.log2 m - 63; let m := Nat.toUInt64 (m >>> s); let e := e + ↑s; Float.scaleB (UInt64.toFloat m) e

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

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

Equations

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

def Float.ofInt : Int → Float

Equations

• Float.ofInt x = match x with | Int.ofNat n => Float.ofNat n | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))

instance instOfNatFloat {n : Nat} : OfNat Float n

Equations

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

@[inline, reducible]

abbrev Nat.toFloat (n : Nat) : Float

Equations

• Nat.toFloat n = Float.ofNat n