typify_universal_set : bool ref
Determines whether the universe set on a type is printed just as the type.
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
- FAILURE CONDITIONS
Note that having this setting is quite useful here:
val it : thm =
|- !x y. x = y <=> (!i. 1 <= i /\ i <= dimindex (:B) ==> x $ i = y $ i)
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.
- SEE ALSO
pp_print_term, prebroken_binops, print_all_thm,
print_unambiguous_comprehensions, reverse_interface_mapping, unspaced_binops.