624 following auxiliary constants are introduced: |
624 following auxiliary constants are introduced: |
625 |
625 |
626 \begin{itemize} |
626 \begin{itemize} |
627 \setlength{\itemsep}{0pt} |
627 \setlength{\itemsep}{0pt} |
628 |
628 |
629 \item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar |
629 \item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar |
630 @{text case}--@{text of} syntax) |
630 @{text case}--@{text of} syntax) |
631 |
631 |
632 \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, |
632 \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, |
633 @{text "t.is_C\<^sub>n"} |
633 @{text "t.is_C\<^sub>n"} |
634 |
634 |
642 |
642 |
643 \item \relax{Map function} (or \relax{functorial action}): @{text t.map_t} |
643 \item \relax{Map function} (or \relax{functorial action}): @{text t.map_t} |
644 |
644 |
645 \item \relax{Relator}: @{text t.rel_t} |
645 \item \relax{Relator}: @{text t.rel_t} |
646 |
646 |
647 \item \relax{Iterator}: @{text t.t_fold} |
647 \item \relax{Iterator}: @{text t.fold_t} |
648 |
648 |
649 \item \relax{Recursor}: @{text t.t_rec} |
649 \item \relax{Recursor}: @{text t.rec_t} |
650 |
650 |
651 \end{itemize} |
651 \end{itemize} |
652 |
652 |
653 \noindent |
653 \noindent |
654 The case combinator, discriminators, and selectors are collectively called |
654 The case combinator, discriminators, and selectors are collectively called |
912 written to call the old ML interfaces will need to be adapted to the new |
912 written to call the old ML interfaces will need to be adapted to the new |
913 interfaces. Little has been done so far in this direction. Whenever possible, it |
913 interfaces. Little has been done so far in this direction. Whenever possible, it |
914 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype} |
914 is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype} |
915 to register new-style datatypes as old-style datatypes. |
915 to register new-style datatypes as old-style datatypes. |
916 |
916 |
917 \item \emph{The recursor @{text "t_rec"} has a different signature for nested |
917 \item \emph{The constants @{text "t_case"} and @{text "t_rec"} are now called |
|
918 @{text "case_t"} and @{text "rec_t"}. |
|
919 |
|
920 \item \emph{The recursor @{text "rec_t"} has a different signature for nested |
918 recursive datatypes.} In the old package, nested recursion through non-functions |
921 recursive datatypes.} In the old package, nested recursion through non-functions |
919 was internally reduced to mutual recursion. This reduction was visible in the |
922 was internally reduced to mutual recursion. This reduction was visible in the |
920 type of the recursor, used by \keyw{primrec}. Recursion through functions was |
923 type of the recursor, used by \keyw{primrec}. Recursion through functions was |
921 handled specially. In the new package, nested recursion (for functions and |
924 handled specially. In the new package, nested recursion (for functions and |
922 non-functions) is handled in a more modular fashion. The old-style recursor can |
925 non-functions) is handled in a more modular fashion. The old-style recursor can |