jakezweifler

Missing translations from IR to R

1

https://github.com/coq-community/corn/blob/af4b86e6ad6cfd242562f9c33c0e438298fc4e1f/coq_reals/Rreals_iso.v#L261 While trying to translate between Coquelicot and corn's complex numbers, I noticed that some of the translations were missing from Rreals_iso.v. Specifically, the translations mapping from IR to R...