For decimal and scientific numbers (e.g., 1.23
, 3.12e10
).
Examples:
OfScientific.ofScientific 123 true 2
represents1.23
OfScientific.ofScientific 121 false 100
represents121e100
Instances
Computes m * 2^e
.
Equations
- Float.ofBinaryScientific m e = let s := m.log2 - 63; let m := (m >>> s).toUInt64; let e := e + ↑s; m.toFloat.scaleB e
Instances For
@[defaultInstance 501]
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]
Equations
Instances For
Equations
- Float.ofInt x = match x with | Int.ofNat n => Float.ofNat n | Int.negSucc n => (Float.ofNat n.succ).neg
Instances For
Equations
- instOfNatFloat = { ofNat := Float.ofNat n }