xxyzzn

A Rationals module that TLC can handle might be useful, but isn’t needed for the applications Andrew mentions. Programs generally implement them using only integer arithmetic with operators that are...

Integer division is already in the module—probably defined in the Naturals module that is imported by the Integers module. (It’s written \div.) It is impossible to directly write an irrational...

My point is not that TLC should not handle rationals. It’s that if it’s going to handle rationals, there’s no reason not to have it handle all reals. There are...