equal
deleted
inserted
replaced
5 \isadelimtheory |
5 \isadelimtheory |
6 % |
6 % |
7 \endisadelimtheory |
7 \endisadelimtheory |
8 % |
8 % |
9 \isatagtheory |
9 \isatagtheory |
|
10 \isamarkupfalse% |
10 % |
11 % |
11 \endisatagtheory |
12 \endisatagtheory |
12 {\isafoldtheory}% |
13 {\isafoldtheory}% |
13 % |
14 % |
14 \isadelimtheory |
15 \isadelimtheory |
15 % |
16 % |
16 \endisadelimtheory |
17 \endisadelimtheory |
17 \isamarkuptrue% |
|
18 % |
18 % |
19 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
20 \index{datatypes!nested}% |
20 \index{datatypes!nested}% |
21 In \S\ref{sec:nested-datatype} we defined the datatype of terms% |
21 In \S\ref{sec:nested-datatype} we defined the datatype of terms% |
22 \end{isamarkuptext}% |
22 \end{isamarkuptext}% |
23 \isamarkupfalse% |
23 \isamarkuptrue% |
24 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}\isamarkuptrue% |
24 \isacommand{datatype}\isamarkupfalse% |
25 % |
25 \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequoteopen}term{\isachardoublequoteclose}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequoteclose}% |
26 \begin{isamarkuptext}% |
26 \begin{isamarkuptext}% |
27 \noindent |
27 \noindent |
28 and closed with the observation that the associated schema for the definition |
28 and closed with the observation that the associated schema for the definition |
29 of primitive recursive functions leads to overly verbose definitions. Moreover, |
29 of primitive recursive functions leads to overly verbose definitions. Moreover, |
30 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
30 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
32 and prove many standard properties of list reversal all over again. |
32 and prove many standard properties of list reversal all over again. |
33 We will now show you how \isacommand{recdef} can simplify |
33 We will now show you how \isacommand{recdef} can simplify |
34 definitions and proofs about nested recursive datatypes. As an example we |
34 definitions and proofs about nested recursive datatypes. As an example we |
35 choose exercise~\ref{ex:trev-trev}:% |
35 choose exercise~\ref{ex:trev-trev}:% |
36 \end{isamarkuptext}% |
36 \end{isamarkuptext}% |
37 \isamarkupfalse% |
37 \isamarkuptrue% |
38 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
38 \isacommand{consts}\isamarkupfalse% |
|
39 \ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequoteclose}% |
39 \isadelimtheory |
40 \isadelimtheory |
40 % |
41 % |
41 \endisadelimtheory |
42 \endisadelimtheory |
42 % |
43 % |
43 \isatagtheory |
44 \isatagtheory |
|
45 \isamarkupfalse% |
44 % |
46 % |
45 \endisatagtheory |
47 \endisatagtheory |
46 {\isafoldtheory}% |
48 {\isafoldtheory}% |
47 % |
49 % |
48 \isadelimtheory |
50 \isadelimtheory |