typify_universal_set : bool ref

SYNOPSIS

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.