search

coq-community / corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
http://c-corn.github.io/
GNU General Public License v2.0
108 stars 43 forks source link

Missing translations from IR to R #164

Open jakezweifler opened 3 years ago

jakezweifler commented 3 years ago

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 were not present for multiplication, negation, etc... although their corresponding theorems in R_morphism.v exist already. Because the lemmas already exist, it would not be too difficult to add the proofs to Rreals_iso.v and I would be happy to make a pull request.

spitters commented 3 years ago

That would be great. Please send a PR.