diff options
Diffstat (limited to 'mppa_k1c/ExtFloats.v')
-rw-r--r-- | mppa_k1c/ExtFloats.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v new file mode 100644 index 00000000..efea278b --- /dev/null +++ b/mppa_k1c/ExtFloats.v @@ -0,0 +1,33 @@ +Require Import Floats. + +Module ExtFloat. +(** TODO check with the actual K1c *) + +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. |