Determines whether the universe set on a type is printed just as the type.
DESCRIPTION
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 CONDITIONS
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.