doc-src/TutorialI/Advanced/advanced.tex
changeset 10654 458068404143
parent 10522 ed3964d1f1a4
child 10885 90695f46440b
     1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -13,9 +13,10 @@
     1.4  \section{Advanced forms of recursion}
     1.5  \index{*recdef|(}
     1.6  
     1.7 -The purpose of this section is to introduce advanced forms of \isacommand{recdef}. It
     1.8 -covers two topics: how to define recursive function over nested recursive datatypes
     1.9 -and how to establish termination by means other than measure functions.
    1.10 +The purpose of this section is to introduce advanced forms of
    1.11 +\isacommand{recdef}: how to define recursive function over nested recursive
    1.12 +datatypes, how to establish termination by means other than measure functions,
    1.13 +and how to deal with partial functions.
    1.14  
    1.15  If, after reading this section, you feel that the definition of recursive
    1.16  functions is overly and maybe unnecessarily complicated by the requirement of
    1.17 @@ -32,12 +33,17 @@
    1.18  \input{Recdef/document/Nested0.tex}
    1.19  \input{Recdef/document/Nested1.tex}
    1.20  \input{Recdef/document/Nested2.tex}
    1.21 -\index{*recdef|)}
    1.22  
    1.23  \subsection{Beyond measure}
    1.24  \label{sec:beyond-measure}
    1.25  \input{Advanced/document/WFrec.tex}
    1.26  
    1.27 +\subsection{Partial functions}
    1.28 +\index{partial function}
    1.29 +\input{Advanced/document/Partial.tex}
    1.30 +
    1.31 +\index{*recdef|)}
    1.32 +
    1.33  \section{Advanced induction techniques}
    1.34  \label{sec:advanced-ind}
    1.35  \index{induction|(}