Give real number type real priority in operator overloading.
DESCRIPTION
Symbols for several arithmetical (`+', `-', ...) and relational (`<',
`>=', ...) operators are overloaded so that they may denote the operators
for several different number systems, particularly num (natural numbers),
int (integers) and real (real numbers). The choice is normally made based
on some known types, or the presence of operators that are not overloaded for
the number systems. (For example, numerals like 42 are always assumed to be
of type num, while the division operator `/' is only defined for real.)
In the absence of any such indication, a default choice will be made. The
effect of prioritize_real() is to make real, the real number type, the
default.
FAILURE CONDITIONS
Never fails.
EXAMPLE
With real priority, most things are interpreted as type real:
# prioritize_real();;
val it : unit = ()
# type_of `x + y`;;
val it : hol_type = `:real`
except that numerals are always of type num, and so:
# type_of `x + 1`;;
val it : hol_type = `:num`
and any explicit type information is used before using the defaults:
# type_of `(x:int) + y`;;
val it : hol_type = `:int`
COMMENTS
It is perhaps better practice to insert types explicitly to avoid dependence on
such defaults, otherwise proofs can become context-dependent. However it is
often very convenient.