equal
deleted
inserted
replaced
575 |
575 |
576 \item All types through which recursion takes place must be new-style datatypes |
576 \item All types through which recursion takes place must be new-style datatypes |
577 or the function type. In principle, it should be possible to support old-style |
577 or the function type. In principle, it should be possible to support old-style |
578 datatypes as well, but the command does not support this yet (and there is |
578 datatypes as well, but the command does not support this yet (and there is |
579 currently no way to register old-style datatypes as new-style datatypes). |
579 currently no way to register old-style datatypes as new-style datatypes). |
|
580 |
|
581 \item The recursor produced for types that recurse through functions has a |
|
582 different signature than with the old package. This makes it impossible to use |
|
583 the old \keyw{primrec} command. |
580 \end{itemize} |
584 \end{itemize} |
581 |
585 |
582 An alternative to @{command datatype_new_compat} is to use the old package's |
586 An alternative to @{command datatype_new_compat} is to use the old package's |
583 \keyw{rep\_datatype} command. The associated proof obligations must then be |
587 \keyw{rep\_datatype} command. The associated proof obligations must then be |
584 discharged manually. |
588 discharged manually. |
1020 "tfold _ (TNil y) = y" | |
1024 "tfold _ (TNil y) = y" | |
1021 "tfold f (TCons x xs) = f x (tfold f xs)" |
1025 "tfold f (TCons x xs) = f x (tfold f xs)" |
1022 |
1026 |
1023 text {* |
1027 text {* |
1024 \noindent |
1028 \noindent |
1025 The next example is not primitive recursive, but it can be defined easily using |
1029 The next example is defined using \keyw{fun} to escape the syntactic |
1026 \keyw{fun}. The @{command datatype_new_compat} command is needed to register |
1030 restrictions imposed on primitive recursive functions. The |
1027 new-style datatypes for use with \keyw{fun} and \keyw{function} |
1031 @{command datatype_new_compat} command is needed to register new-style datatypes |
|
1032 for use with \keyw{fun} and \keyw{function} |
1028 (Section~\ref{sssec:datatype-new-compat}): |
1033 (Section~\ref{sssec:datatype-new-compat}): |
1029 *} |
1034 *} |
1030 |
1035 |
1031 datatype_new_compat nat |
1036 datatype_new_compat nat |
1032 |
1037 |