Documentation

Init.Data.OfScientific

class OfScientific (α : Type u) :

Type u

ofScientific : Nat → Bool → Nat → α

Instances

instOfScientificFloat

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

Equations

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

Computes m*2^e.

@[defaultInstance 1001]

instance instOfScientificFloat :

OfScientific Float

Equations

instOfScientificFloat = { ofScientific := fun m s e => if s = true then let s := 64 - Nat.log2 m; let m := m <<< (3 * e + s) / 5 ^ e; Float.ofBinaryScientific m (-4 * Int.ofNat e - Int.ofNat s) else Float.ofBinaryScientific (m * 5 ^ e) (Int.ofNat e) }

def Float.ofNat (n : Nat) :

Equations

Float.ofNat n = OfScientific.ofScientific n false 0

def Float.ofInt :

Equations

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

instance instOfNatFloat {n : Nat} :

Equations

instOfNatFloat = { ofNat := Float.ofNat n }

@[inline]

abbrev Nat.toFloat (n : Nat) :

Equations

Nat.toFloat n = Float.ofNat n