equal
deleted
inserted
replaced
526 \subsection*{Exercises} |
526 \subsection*{Exercises} |
527 |
527 |
528 \exercise\label{exe:tree0} |
528 \exercise\label{exe:tree0} |
529 Define a datatype @{text tree0} of binary tree skeletons which do not store |
529 Define a datatype @{text tree0} of binary tree skeletons which do not store |
530 any information, neither in the inner nodes nor in the leaves. |
530 any information, neither in the inner nodes nor in the leaves. |
531 Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the total number |
531 Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of |
532 all nodes (inner nodes and leaves) in such a tree. |
532 all nodes (inner nodes and leaves) in such a tree. |
533 Consider the following recursive function: |
533 Consider the following recursive function: |
534 *} |
534 *} |
535 (*<*) |
535 (*<*) |
536 datatype tree0 = Tip | Node tree0 tree0 |
536 datatype tree0 = Tip | Node tree0 tree0 |
569 that evaluates a polynomial at the given value. |
569 that evaluates a polynomial at the given value. |
570 Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}} |
570 Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}} |
571 that transforms an expression into a polynomial. This may require auxiliary |
571 that transforms an expression into a polynomial. This may require auxiliary |
572 functions. Prove that @{text coeffs} preserves the value of the expression: |
572 functions. Prove that @{text coeffs} preserves the value of the expression: |
573 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.} |
573 \mbox{@{prop"evalp (coeffs e) x = eval e x"}.} |
574 Hint: consider the hint in \autoref{exe:tree0}. |
574 Hint: consider the hint in Exercise~\ref{exe:tree0}. |
575 \endexercise |
575 \endexercise |
576 *} |
576 *} |
577 (*<*) |
577 (*<*) |
578 end |
578 end |
579 (*>*) |
579 (*>*) |