ind

Type.ind : hol_type

Basic type constant.

The ML variable Type.ind is bound to the HOL type constant ind. The axiom INFINITY_AX in boolTheory states that ind represents an infinite set of individuals.

See also

Type.bool, Type.-->