Computational Floating Point Design

1. We have the lean `Float` which are doubles.
2. These are converted into a `PackedFloat`, that separates the IEEE components of a float into `(sign, mantissa, exponent)`.
3. Following this, for computation, these are converted into an `EDyadic`, which is an inductive that can either be `nan`, `infinity (sign : Bool)`, `zero (sign : Bool)`, or `number (n : Dyadic)`. This provides the ability to perfectly represent numbers of the form $$k \times 2^n$$.
4. Now, on `Dyadic`, we will implement `round : Dyadic -> (enew : Int) (snew : Nat) -> ExtDyadic`, which provides an `ExtDyadic` that is rounded, i.e., there exits a IEEE floating point in `(enew, snew)` that is represented by this `ExtDyadic`.
5. Finally, we have `pack : ExtDyadic -> Option PackedFloat` that packs a number back into an IEEE float.

Overall, this representation uses `Dyadic` for scientific notation representation, and builds the theory of packing and unpacking.