Computing with Classical Real Numbers

Cezary Kaliszyk, Russell O'Connor

There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN lib…