Commit 13b3bd9f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Beautify inductive definitions.

parent cdfa7d0e
......@@ -29,7 +29,7 @@ Notation bpow := (bpow beta).
Variable emin : Z.
Inductive FIX_format (x : R) : Prop :=
FIX_spec : forall f : float beta,
FIX_spec (f : float beta) :
x = F2R f -> (Fexp f = emin)%Z -> FIX_format x.
Definition FIX_exp (e : Z) := emin.
......
......@@ -32,7 +32,7 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FLT_format (x : R) : Prop :=
FLT_spec : forall f : float beta,
FLT_spec (f : float beta) :
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z -> FLT_format x.
......
......@@ -35,7 +35,7 @@ Class Prec_gt_0 :=
Context { prec_gt_0_ : Prec_gt_0 }.
Inductive FLX_format (x : R) : Prop :=
FLX_spec : forall f : float beta,
FLX_spec (f : float beta) :
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.
Definition FLX_exp (e : Z) := (e - prec)%Z.
......@@ -132,7 +132,7 @@ Qed.
(** unbounded floating-point format with normal mantissas *)
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec : forall f : float beta,
FLXN_spec (f : float beta) :
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
......
......@@ -32,7 +32,7 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FTZ_format (x : R) : Prop :=
FTZ_spec : forall f : float beta,
FTZ_spec (f : float beta) :
x = F2R f ->
(x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z ->
......
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