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
|
\DOC show_types
\TYPE {show_types : (bool -> bool)}
\SYNOPSIS
Turns printing of HOL types (in terms) on/off.
\DESCRIBE
Normally HOL types in terms are not printed, since this makes terms hard to
read. Type printing is enabled by {show_types true}, and disabled by
{show_types false}. When printing of types is enabled, not all variables and
constants are annotated with a type. The intention is to provide sufficient
type information to remove any ambiguities without swamping the term with type
information.
\FAILURE
Never fails.
\EXAMPLE
{
#BOOL_CASES_AX;;
|- !t. (t = T) \/ (t = F)
#show_types true;;
false : bool
#BOOL_CASES_AX;;
|- !(t:bool). (t = T) \/ (t = F)
}
\COMMENTS
It is possible to construct an abstraction in which the bound variable has the
same name but a different type to a variable in the body. In such a case the
two variables are considered to be distinct. Without type information such a
term can be very misleading, so it might be a good idea to provide type
information for the free variable whether or not printing of types is enabled.
\SEEALSO
print_term.
\ENDDOC
|
