equal
deleted
inserted
replaced
27 \end{isamarkuptext}% |
27 \end{isamarkuptext}% |
28 \isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
28 \isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
29 {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}% |
29 {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}% |
30 \begin{isamarkuptext}% |
30 \begin{isamarkuptext}% |
31 The rest of this section is devoted to the question of how to define |
31 The rest of this section is devoted to the question of how to define |
32 partial recursive functions by other means that non-exhaustive pattern |
32 partial recursive functions by other means than non-exhaustive pattern |
33 matching.% |
33 matching.% |
34 \end{isamarkuptext}% |
34 \end{isamarkuptext}% |
35 % |
35 % |
36 \isamarkupsubsubsection{Guarded Recursion% |
36 \isamarkupsubsubsection{Guarded Recursion% |
37 } |
37 } |