equal
deleted
inserted
replaced
9 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
9 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
10 quadratic. A linear time version of \isa{flatten} again reqires an extra |
10 quadratic. A linear time version of \isa{flatten} again reqires an extra |
11 argument, the accumulator:% |
11 argument, the accumulator:% |
12 \end{isamarkuptext}% |
12 \end{isamarkuptext}% |
13 \isamarkuptrue% |
13 \isamarkuptrue% |
14 \isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
14 \isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
15 \isamarkupfalse% |
15 \isamarkupfalse% |
16 % |
16 % |
17 \begin{isamarkuptext}% |
17 \begin{isamarkuptext}% |
18 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
18 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |