Commit 14d91090 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fixed duplicated radix arguments.

parent 03ad1620
......@@ -2,16 +2,15 @@ Require Import Flocq_Raux.
Section Def.
Variable beta: radix.
Notation bpow := (epow beta).
Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }.
Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].
Definition F2R {beta : radix} (f : float beta) :=
(Z2R (Fnum f) * bpow (Fexp f))%R.
Variable beta : radix.
Definition F2R (f : float beta) :=
(Z2R (Fnum f) * epow beta (Fexp f))%R.
(* A rounding mode will be a function, ie a R -> R *)
(* It will then have to satisfy a number of properties on a given domain D *)
......@@ -56,6 +55,10 @@ Definition FIX_RoundingModeP (emin : Z) (rnd : R -> R):=
End Def.
Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].
Implicit Arguments F2R [[beta]].
Section RND.
(* property of being a rounding toward -inf *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment