doc-src/TutorialI/Advanced/advanced.tex
changeset 10186 499637e8f2c6
parent 10178 aecb5bf6f76f
child 10187 0376cccd9118
equal deleted inserted replaced
10185:c452fea3ce74 10186:499637e8f2c6
    10 required for parts of the section on recursion.
    10 required for parts of the section on recursion.
    11 
    11 
    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 \label{sec:advanced-recdef}
       
    16 \index{*recdef|(}
    15 \index{*recdef|(}
       
    16 
       
    17 \subsection{Recursion over nested datatypes}
       
    18 \label{sec:nested-recdef}
    17 \input{Recdef/document/Nested0.tex}
    19 \input{Recdef/document/Nested0.tex}
    18 \input{Recdef/document/Nested1.tex}
    20 \input{Recdef/document/Nested1.tex}
    19 \input{Recdef/document/Nested2.tex}
    21 \input{Recdef/document/Nested2.tex}
    20 \index{*recdef|)}
    22 \index{*recdef|)}
       
    23 
       
    24 \subsection{Beyond measure}
       
    25 \label{sec:wellfounded}
       
    26 \input{Recdef/document/WFrec.tex}
    21 
    27 
    22 \section{Advanced induction techniques}
    28 \section{Advanced induction techniques}
    23 \label{sec:advanced-ind}
    29 \label{sec:advanced-ind}
    24 \index{induction|(}
    30 \index{induction|(}
    25 \input{Misc/document/AdvancedInd.tex}
    31 \input{Misc/document/AdvancedInd.tex}