data Natural = Zero | Successor Natural nfold :: .. -> .. -> .. nfold z s Zero = .. nfold z s ( Successor x ) = .. plus x = nfold x ( \ y p -> Successor p ) times = nfold ( \ y -> Zero ) ( \ x p y -> ... ) power b = nfold ( ... ) ( \ x p -> ... )So definierte Funktionen sind ,,automatisch`` terminierend.