Commit e9ef2828 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Removed obsolete comment.

parent 6bfb29b6
......@@ -12,16 +12,10 @@ 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 *)
(* The domain will be used to formalize Overflow, flush to zero... *)
Definition MonotoneP (rnd : R -> R) :=
forall x y : R,
(x <= y)%R -> (rnd x <= rnd y)%R.
Definition IdempotentP (F : R -> Prop) (rnd : R -> R) :=
(forall x : R, F (rnd x))
/\ (forall x : R, F x -> rnd x = x).
......
Markdown is supported
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