12 \input{Advanced/document/simp.tex} |
12 \input{Advanced/document/simp.tex} |
13 |
13 |
14 \section{Advanced forms of recursion} |
14 \section{Advanced forms of recursion} |
15 \index{*recdef|(} |
15 \index{*recdef|(} |
16 |
16 |
|
17 The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It |
|
18 covers two topics: how to define recursive function over nested recursive datatypes |
|
19 and how to establish termination by means other than measure functions. |
|
20 |
17 \subsection{Recursion over nested datatypes} |
21 \subsection{Recursion over nested datatypes} |
18 \label{sec:nested-recdef} |
22 \label{sec:nested-recdef} |
19 \input{Recdef/document/Nested0.tex} |
23 \input{Recdef/document/Nested0.tex} |
20 \input{Recdef/document/Nested1.tex} |
24 \input{Recdef/document/Nested1.tex} |
21 \input{Recdef/document/Nested2.tex} |
25 \input{Recdef/document/Nested2.tex} |
22 \index{*recdef|)} |
26 \index{*recdef|)} |
23 |
27 |
24 \subsection{Beyond measure} |
28 \subsection{Beyond measure} |
25 \label{sec:wellfounded} |
29 \label{sec:wellfounded} |
26 \input{Recdef/document/WFrec.tex} |
30 \input{Advanced/document/WFrec.tex} |
27 |
31 |
28 \section{Advanced induction techniques} |
32 \section{Advanced induction techniques} |
29 \label{sec:advanced-ind} |
33 \label{sec:advanced-ind} |
30 \index{induction|(} |
34 \index{induction|(} |
31 \input{Misc/document/AdvancedInd.tex} |
35 \input{Misc/document/AdvancedInd.tex} |