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.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help