Lines Matching defs:constructors
1430 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.
1499 newly defined type constructors $t@1,\ldots,t@n$, or
1559 \subsubsection{Freeness of the constructors}
1561 The datatype constructors are automatically defined as functions of their
1576 constructors, the datatype package avoids proving them separately if there are
1577 too many constructors. Instead, specific inequalities are proved by a suitable
1637 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt
1640 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
1680 All constructors must be present, their order is fixed, and nested patterns
1742 constructors, and the theorems listed in the previous section.
1759 constructors of the datatype suffices.
1763 If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal