equal
deleted
inserted
replaced
18 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
19 \noindent In Exercise~\ref{ex:Tree} we defined a function |
19 \noindent In Exercise~\ref{ex:Tree} we defined a function |
20 \isa{flatten} from trees to lists. The straightforward version of |
20 \isa{flatten} from trees to lists. The straightforward version of |
21 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
21 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
22 quadratic. A linear time version of \isa{flatten} again reqires an extra |
22 quadratic. A linear time version of \isa{flatten} again reqires an extra |
23 argument, the accumulator:% |
23 argument, the accumulator. Define% |
24 \end{isamarkuptext}% |
24 \end{isamarkuptext}% |
25 \isamarkuptrue% |
25 \isamarkuptrue% |
26 \isacommand{consts}\isamarkupfalse% |
26 flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}% |
27 \ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}% |
|
28 \begin{isamarkuptext}% |
27 \begin{isamarkuptext}% |
29 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
28 \noindent and prove% |
30 \end{isamarkuptext}% |
29 \end{isamarkuptext}% |
31 \isamarkuptrue% |
30 \isamarkuptrue% |
32 % |
31 % |
33 \isadelimproof |
32 \isadelimproof |
34 % |
33 % |