Documentation
Init
.
Data
.
Float
.
Model
.
Unpacked
.
Operations
.
OfScientific
Search
return to top
source
Imports
Init.Data.Nat.Bitwise.Lemmas
Init.Data.Float.Model.Unpacked.Operations.Div
Init.Data.Float.Model.Unpacked.Operations.Mul
Imported by
Float
.
Model
.
UnpackedFloat
.
ofScientific
source
def
Float
.
Model
.
UnpackedFloat
.
ofScientific
(
spec
:
Format
)
(
m
:
Nat
)
(
e
:
Int
)
:
UnpackedFloat
Computes
m * 10 ^ e
.
Instances For