Library Flocq.Core.FIX

This file is part of the Flocq formalization of floating-point arithmetic in Coq:
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Fixed-point format

Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE.

Section RND_FIX.

Variable beta : radix.

Notation bpow := (bpow beta).

Variable emin : Z.

Inductive FIX_format (x : R) : Prop :=
  FIX_spec (f : float beta) :
    x = F2R f (Fexp f = emin)%Z FIX_format x.

Definition FIX_exp (e : Z) := emin.

Properties of the FIX format