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
|
\DOC type_invention_error
\TYPE {type_invention_error : bool ref}
\SYNOPSIS
Determines if invented type variables are treated as an error.
\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_error} determines whether in such cases the term parser treats
it as an error. The default is {false}, since sometimes the invention of type
variables is immaterial, e.g. in ad-hoc logical lemmas used inside a proof.
However, to enforce a more careful style, set it 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. In the normal course of events this merely results in a
warning (see {type_invention_warning} to remove even this warning):
{
# let tm = `x = x`;;
Warning: inventing type variables
val tm : term = `x = x`
}
\noindent whereas if {type_invention_error} is set to {true}, the term parser
fails with an error message:
{
# type_invention_error := true;;
val it : unit = ()
# let tm = `x = x`;;
Exception: Failure "typechecking error (cannot infer type of variables)".
}
\noindent You can avoid the error by explicitly giving appropriate types or
type variables yourself:
{
# let tm = `(x:int) = x`;;
val tm : term = `x = x`
}
\SEEALSO
retypecheck, term_of_preterm, type_invention_warning.
\ENDDOC
|
