doc-src/TutorialI/Advanced/document/Partial.tex
changeset 11157 0d94005e374c
parent 11149 e258b536a137
child 11158 5652018b809a
equal deleted inserted replaced
11156:1d1d9f60c29b 11157:0d94005e374c
   152 That is, \isa{while\ b\ c\ s} is equivalent to the imperative program
   152 That is, \isa{while\ b\ c\ s} is equivalent to the imperative program
   153 \begin{verbatim}
   153 \begin{verbatim}
   154      x := s; while b(x) do x := c(x); return x
   154      x := s; while b(x) do x := c(x); return x
   155 \end{verbatim}
   155 \end{verbatim}
   156 In general, \isa{s} will be a tuple (better still: a record). As an example
   156 In general, \isa{s} will be a tuple (better still: a record). As an example
   157 consider the tail recursive variant of function \isa{find} above:%
   157 consider the following definition of function \isa{find} above:%
   158 \end{isamarkuptext}%
   158 \end{isamarkuptext}%
   159 \isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
   159 \isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
   160 \ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
   160 \ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
   161 \ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   161 \ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
   162 \begin{isamarkuptext}%
   162 \begin{isamarkuptext}%