Conversion of Real to Float (library)

We define all the specific real-to-float translations here. Any issues with real-to-float are likely due to missing translations. Users need to make sure that the types of the translations correspond to the required types. For example, an expression of type ℝ needs to map to an expression of type Float, and an expression of type Fin n → ℝ → ℝ needs to map to an expression of type Fin n → Float → Float.