equal
deleted
inserted
replaced
11 text{*\noindent |
11 text{*\noindent |
12 and closed with the observation that the associated schema for the definition |
12 and closed with the observation that the associated schema for the definition |
13 of primitive recursive functions leads to overly verbose definitions. Moreover, |
13 of primitive recursive functions leads to overly verbose definitions. Moreover, |
14 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
14 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
15 you needed to declare essentially the same function as @{term"rev"} |
15 you needed to declare essentially the same function as @{term"rev"} |
16 and prove many standard properties of list reverse all over again. |
16 and prove many standard properties of list reversal all over again. |
17 We will now show you how \isacommand{recdef} can simplify |
17 We will now show you how \isacommand{recdef} can simplify |
18 definitions and proofs about nested recursive datatypes. As an example we |
18 definitions and proofs about nested recursive datatypes. As an example we |
19 choose exercise~\ref{ex:trev-trev}: |
19 choose exercise~\ref{ex:trev-trev}: |
20 *} |
20 *} |
21 |
21 |