The infix operators for reals are awkward
The real.Real
module defines infix binary operators on reals that have the same names as the integer ones. In case the user wishes to use both integer and real binary operators, (+.)
and so on are defined in a second module RealInfix
. But I feel this introduces more issues than it solves. The lemmas in other real theories (such as real.Square
, real.PowerReal
and so on use the real.Real
operators. But in most nontrivial programs, the user really will use both Int
and Real
, so their lemmas will use the RealInfix
operators. This mismatch causes some lemma instantiation issues.
My impression is that few programs will manage to use real.Real
operators (that is, not import int.Int at all or namespace it), and that we'd be better off always having points in the binary operators rather than having two separate sets of operators.