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
53
54
55
56
|
\DOC prioritize_overload
\TYPE {prioritize_overload : hol_type -> unit}
\SYNOPSIS
Give overloaded constants involving a given type priority in operator
overloading.
\DESCRIBE
In general, overloaded operators in the concrete syntax, such as `{+}', are
ambiguous, referring to one of several underlying constants. 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_overload `:ty`} is to run through the
overloaded symbols making the first instance of each where the generic type
variables in the type skeleton are replaced by type {`:ty`} the first priority
when no other indication is made.
\FAILURE
Never fails.
\EXAMPLE
With real priority, most things are interpreted as type {real}:
{
# prioritize_overload `:real`;;
val it : unit = ()
# type_of `x + y`;;
val it : hol_type = `:real`
}
\noindent By making {int} the priority, everything is interpreted as {int}:
{
# prioritize_overload `:int`;;
val it : unit = ()
# type_of `x + y`;;
val it : hol_type = `:int`
}
\noindent unless there is some explicit type information to the contrary:
{
# type_of `(x:real) + y`;;
val it : hol_type = `:real`
}
\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_real, the_implicit_types, the_overload_skeletons.
\ENDDOC
|
