max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: Float.abs function (#1514)

Browse source
This commit is contained in:
Fynn Schmitt-Ulms 2022-08-25 21:45:46 -04:00 • committed by GitHub
parent 65f9344f01
commit 064ab16791
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data/Float.lean
View file

@ -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⟩

4
tests/compiler/float.lean
View file

@ -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]

1
tests/compiler/float.lean.expected.out
View file

@ -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]