equal
deleted
inserted
replaced
793 |
793 |
794 Have a look at these files and try to solve the following two exercises: |
794 Have a look at these files and try to solve the following two exercises: |
795 |
795 |
796 \begin{exercise}\label{fun:revsum} |
796 \begin{exercise}\label{fun:revsum} |
797 Write a function @{text "rev_sum : term -> term"} that takes a |
797 Write a function @{text "rev_sum : term -> term"} that takes a |
798 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero) |
798 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
799 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
799 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
800 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
800 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
801 associates to the left. Try your function on some examples. |
801 associates to the left. Try your function on some examples. |
802 \end{exercise} |
802 \end{exercise} |
803 |
803 |