/Prelude-v17.0.0/Natural/toDouble

Copy path to clipboard

Examples

toDouble 3 ≡ 3.0
toDouble 0 ≡ 0.0

Source

{-
Convert a `Natural` number to the corresponding `Double`
-}
let toDouble
: Natural → Double
= λ(n : Natural) → Integer/toDouble (Natural/toInteger n)

let example0 = assert : toDouble 3 ≡ 3.0

let example1 = assert : toDouble 0 ≡ 0.0

in toDouble