blob: 090844f6920e1e4fc43e76612fed7bf6cd69c30c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Require Import Floats.
Module ExtFloat.
(** TODO check with the actual K1c;
this is what happens on x86 and may be inappropriate. *)
Definition min (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float) (y : float) : float :=
match Float.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
End ExtFloat.
Module ExtFloat32.
(** TODO check with the actual K1c *)
Definition min (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Lt => x
| Some Gt | None => y
end.
Definition max (x : float32) (y : float32) : float32 :=
match Float32.compare x y with
| Some Eq | Some Gt => x
| Some Lt | None => y
end.
End ExtFloat32.
|