Roger, David, > On 2 Nov 2019, at 18:45, Roger Bishop Jones <[email protected]> wrote: > > Oops. > > On 02/11/2019 17:25, Roger Bishop Jones wrote: >> How about working in theory "ℚ"? > Great idea, apart from the fact that it doesn't exist!
That's right: we don't provide a type ℚ of rationals. The approach I took to defining the type ℝ of reals doesn't construct the rationals first. A type of rationals could easily be provided as a subtype of the reals, but I have never felt the need for it: if I need to work with the rationals I just treat them as a subset of the reals. Regards, Rob. _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
