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 type_invention_warning
\TYPE {type_invention_warning : bool ref}
\SYNOPSIS
Determined if user is warned about invented type variables.
\DESCRIBE
If HOL Light is unable to assign specific types to a term entered in quotation,
it will invent its own type variables to use in the most general type. The flag
{type_invention_warning} determines whether the user is warned in such
situations. The default is {true}, since this can often indicate a user error
(e.g. the user forgot to define a constant before using it in a term or
overlooked more general types than expected). To disable the warnings, set it
to {false}, while to make the checking even more rigorous and treat it as an
error, set {type_invention_error} to {true}.
\FAILURE
Not applicable.
\EXAMPLE
When the following term is entered, HOL Light invents a type variable to use as
the most general type:
{
# let tm = `x IN s`;;
Warning: inventing type variables
val tm : term = `x IN s`
}
\noindent which are not particularly intuitive, as you can see:
{
# map dest_var (frees tm);;
val it : (string * hol_type) list =
[("x", `:?47676`); ("s", `:?47676->bool`)]
}
\noindent You can avoid this by explicitly giving appropriate types or type
variables yourself:
{
# let tm = `(x:A) IN s`;;
val tm : term = `x IN s`
}
But if you often want to let HOL Light invent types for itself without warning
you, set
{
# type_invention_warning := false;;
val it : unit = ()
}
One reason why you might find the warning more irritating than helpful is if
you are rewriting with ad-hoc set theory lemmas generated like this:
{
# SET_RULE `x IN UNIONS (a INSERT t) <=> x IN UNIONS t \/ x IN a`;;
}
\SEEALSO
retypecheck, term_of_preterm, type_invention_error.
\ENDDOC
|
