equal
deleted
inserted
replaced
117 Correct this statement (you will find that it does not type-check), |
117 Correct this statement (you will find that it does not type-check), |
118 strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition; |
118 strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition; |
119 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
119 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
120 \end{exercise} |
120 \end{exercise} |
121 \begin{exercise}\label{ex:trev-trev} |
121 \begin{exercise}\label{ex:trev-trev} |
122 Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term} |
122 Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term} |
123 that recursively reverses the order of arguments of all function symbols in a |
123 that recursively reverses the order of arguments of all function symbols in a |
124 term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}. |
124 term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}. |
125 \end{exercise} |
125 \end{exercise} |
126 |
126 |
127 The experienced functional programmer may feel that our definition of |
127 The experienced functional programmer may feel that our definition of |