1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\DOC prioritize_real
\TYPE {prioritize_real : unit -> unit}
\SYNOPSIS
Give real number type {real} priority in operator overloading.
\DESCRIBE
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
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`
}
\noindent except that numerals are always of type {num}, and so:
{
# type_of `x + 1`;;
val it : hol_type = `:num`
}
\noindent 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.
\SEEALSO
make_overloadable, overload_interface, prioritize_int, prioritize_num,
prioritize_overload, the_overload_skeletons.
\ENDDOC
|
