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
|
\DOC typify_universal_set
\TYPE {typify_universal_set : bool ref}
\SYNOPSIS
Determines whether the universe set on a type is printed just as the type.
\DESCRIBE
The reference variable {typify_universal_set} is one of several
settable parameters controlling printing of terms by {pp_print_term}, and hence
the automatic printing of terms and theorems at the toplevel. When it is
{true}, as it is by default, any universal set {UNIV:A->bool} ({UNIV} is a
predefined set constant valid over all types) is printed just as {(:A)}. When
{typify_universal_set} is {false}, it is printed as {UNIV}, just as for any
other constant.
\FAILURE
Not applicable.
\EXAMPLE
Note that having this setting is quite useful here:
{
# CART_EQ;;
val it : thm =
|- !x y. x = y <=> (!i. 1 <= i /\ i <= dimindex (:B) ==> x $ i = y $ i)
}
\USES
HOL Light's Cartesian power type (constructor `{^}') uses a type to index the
power. When this flag is {true}, formulas often become easier to understand
when printed, as in the above example.
\SEEALSO
pp_print_term, prebroken_binops, print_all_thm,
print_unambiguous_comprehensions, reverse_interface_mapping, unspaced_binops.
\ENDDOC
|
