From 29091abb98c602ca91b3689253ed70fd2f67ba42 Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Fri, 7 Sep 2018 09:40:16 -0700 Subject: [PATCH] Add `{Integer,Natural}/toDouble` I had forgotten to mirror these to the official Prelude when I added them to the Prelude used by the Haskell implementation --- Integer/toDouble | 12 ++++++++++++ Natural/toDouble | 16 ++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 Integer/toDouble create mode 100644 Natural/toDouble diff --git a/Integer/toDouble b/Integer/toDouble new file mode 100644 index 0000000..8b30c78 --- /dev/null +++ b/Integer/toDouble @@ -0,0 +1,12 @@ +{- +Convert an `Integer` to the corresponding `Double` + +Examples: + +``` +./toDouble -3 = -3.0 + +./toDouble +2 = 2.0 +``` +-} +let toDouble : Integer → Double = Integer/toDouble in toDouble diff --git a/Natural/toDouble b/Natural/toDouble new file mode 100644 index 0000000..12f9392 --- /dev/null +++ b/Natural/toDouble @@ -0,0 +1,16 @@ +{- +Convert a `Natural` number to the corresponding `Double` + +Examples: + +``` +./toDouble 3 = 3.0 + +./toDouble 0 = 0.0 +``` +-} + let toDouble + : Natural → Double + = λ(n : Natural) → Integer/toDouble (Natural/toInteger n) + +in toDouble