Module ExtFloats

From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
                          Binary Round_odd.
Require Import Floats Integers ZArith.

Module ExtFloat.

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.

Definition one := Float.of_int (Int.repr (1%Z)).
End ExtFloat.

Module ExtFloat32.

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.

Definition one := Float32.of_int (Int.repr (1%Z)).
Definition inv (x : float32) : float32 :=
  Float32.div one x.
End ExtFloat32.