From b8ea55c989daab53d1ddad18aca5556bb252bb59 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Apr 2020 15:19:28 -0700
Subject: [PATCH] feat: expose some transcendental functions from the C library

cc @dselsam
---
 src/Init/Data/Float.lean   | 24 ++++++++++++++++++++++++
 tests/lean/run/float1.lean |  8 ++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 tests/lean/run/float1.lean

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 8067c4c848..77bb3294d3 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -73,3 +73,27 @@ instance : HasToString Float := ⟨Float.toString⟩
 
 abbrev Nat.toFloat (n : Nat) : Float :=
 Float.ofNat n
+
+@[extern "sin"] constant Float.sin : Float → Float := arbitrary _
+@[extern "cos"] constant Float.cos : Float → Float := arbitrary _
+@[extern "tan"] constant Float.tan : Float → Float := arbitrary _
+@[extern "asin"] constant Float.asin : Float → Float := arbitrary _
+@[extern "acos"] constant Float.acos : Float → Float := arbitrary _
+@[extern "atan"] constant Float.atan : Float → Float := arbitrary _
+@[extern "atan2"] constant Float.atan2 : Float → Float → Float := arbitrary _
+@[extern "sinh"] constant Float.sinh : Float → Float := arbitrary _
+@[extern "cosh"] constant Float.cosh : Float → Float := arbitrary _
+@[extern "tanh"] constant Float.tanh : Float → Float := arbitrary _
+@[extern "asinh"] constant Float.asinh : Float → Float := arbitrary _
+@[extern "acosh"] constant Float.acosh : Float → Float := arbitrary _
+@[extern "atanh"] constant Float.atanh : Float → Float := arbitrary _
+@[extern "exp"] constant Float.exp : Float → Float := arbitrary _
+@[extern "exp2"] constant Float.exp2 : Float → Float := arbitrary _
+@[extern "log"] constant Float.log : Float → Float := arbitrary _
+@[extern "log2"] constant Float.log2 : Float → Float := arbitrary _
+@[extern "log10"] constant Float.log10 : Float → Float := arbitrary _
+@[extern "pow"] constant Float.pow : Float → Float → Float := arbitrary _
+@[extern "sqrt"] constant Float.sqrt : Float → Float := arbitrary _
+@[extern "cbrt"] constant Float.cbrt : Float → Float := arbitrary _
+
+instance : HasPow Float Float := ⟨Float.pow⟩
diff --git a/tests/lean/run/float1.lean b/tests/lean/run/float1.lean
new file mode 100644
index 0000000000..061a49866b
--- /dev/null
+++ b/tests/lean/run/float1.lean
@@ -0,0 +1,8 @@
+def main : IO Unit := do
+IO.println ((2 : Float).sin);
+IO.println ((2 : Float).cos);
+IO.println ((2 : Float).sqrt);
+IO.println ((2 : Float) ^ (200 : Float));
+pure ()
+
+#eval main