From 064ab1679191cf8e8c68cfd31025ed76798f5e7d Mon Sep 17 00:00:00 2001
From: Fynn Schmitt-Ulms <fynnsu@outlook.com>
Date: Thu, 25 Aug 2022 21:45:46 -0400
Subject: [PATCH] feat: Float.abs function (#1514)

---
 src/Init/Data/Float.lean               | 1 +
 tests/compiler/float.lean              | 4 ++++
 tests/compiler/float.lean.expected.out | 1 +
 3 files changed, 6 insertions(+)

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 99dde56bae..75f2285498 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -129,6 +129,7 @@ instance : ReprAtom Float  := ⟨⟩
 @[extern "ceil"] opaque Float.ceil : Float → Float
 @[extern "floor"] opaque Float.floor : Float → Float
 @[extern "round"] opaque Float.round : Float → Float
+@[extern "fabs"] opaque Float.abs : Float → Float
 
 instance : Pow Float Float := ⟨Float.pow⟩
 
diff --git a/tests/compiler/float.lean b/tests/compiler/float.lean
index a724ff5520..b70268145d 100644
--- a/tests/compiler/float.lean
+++ b/tests/compiler/float.lean
@@ -51,8 +51,12 @@ def tst2 (x : Nat) : IO Unit := do
 def tst3 (xs : List Float) (y : Float) : IO Unit :=
   IO.println (fMap (fun x => x / y) xs)
 
+def tst4 (xs : List Float) : IO Unit :=
+  IO.println (fMap (fun x => x.abs) xs)
+
 def main : IO Unit := do
   tst1
   IO.println "-----"
   tst2 7
   tst3 [3, 4, 7, 8, 9, 11] 2
+  tst4 [3, -3, 0, -0, -1 / 0, -0 / 0]
diff --git a/tests/compiler/float.lean.expected.out b/tests/compiler/float.lean.expected.out
index ee02fed398..52a4306fb2 100644
--- a/tests/compiler/float.lean.expected.out
+++ b/tests/compiler/float.lean.expected.out
@@ -32,3 +32,4 @@ true
 2.333333
 3.500000
 [1.500000, 2.000000, 3.500000, 4.000000, 4.500000, 5.500000]
+[3.000000, 3.000000, 0.000000, 0.000000, inf, NaN]