Lines Matching defs:constructors
1247 and induction rules automatically, as well as the constructors, case operator
1645 However, the package declares the constructors. Here, \isa{Nil} gets type
1674 \subsubsection{Freeness of the constructors}
1679 Because the number of freeness is quadratic in the number of constructors, the
1682 asserting the equality of two datatype constructors, it performs freeness
1758 of the constructors of the two datatypes.
1767 constructors, and the theorems listed in the previous section.
1792 constructors of the datatype suffices.
1825 con_defs \textrm{definitions of the case operator and constructors}
1903 When there are only a few constructors, we might prefer to prove the freenness
1943 This example shows a datatype that consists of 60 constructors:
1957 (on a 1.8GHz machine). The constructors have a balanced representation,
2017 immaterial. For missing constructors, the function is defined to return zero.
2145 the constructors' definitions here. Most (co)inductive definitions omit