equal
deleted
inserted
replaced
1 % |
1 \begin{isabelle}% |
2 \begin{isabellebody}% |
|
3 % |
2 % |
4 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
5 So far, all datatypes had the property that on the right-hand side of their |
4 So far, all datatypes had the property that on the right-hand side of their |
6 definition they occurred only at the top-level, i.e.\ directly below a |
5 definition they occurred only at the top-level, i.e.\ directly below a |
7 constructor. This is not the case any longer for the following model of terms |
6 constructor. This is not the case any longer for the following model of terms |
120 |
119 |
121 Of course, you may also combine mutual and nested recursion. For example, |
120 Of course, you may also combine mutual and nested recursion. For example, |
122 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
121 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
123 expressions as its argument: \isa{Sum "'a aexp list"}.% |
122 expressions as its argument: \isa{Sum "'a aexp list"}.% |
124 \end{isamarkuptext}% |
123 \end{isamarkuptext}% |
125 \end{isabellebody}% |
124 \end{isabelle}% |
126 %%% Local Variables: |
125 %%% Local Variables: |
127 %%% mode: latex |
126 %%% mode: latex |
128 %%% TeX-master: "root" |
127 %%% TeX-master: "root" |
129 %%% End: |
128 %%% End: |