equal
deleted
inserted
replaced
1946 \index{*primrec|)} |
1946 \index{*primrec|)} |
1947 |
1947 |
1948 |
1948 |
1949 \subsection{Well-founded recursive functions} |
1949 \subsection{Well-founded recursive functions} |
1950 \label{sec:HOL:recdef} |
1950 \label{sec:HOL:recdef} |
1951 \index{primitive recursion|(} |
1951 \index{recursion!general|(} |
1952 \index{*recdef|(} |
1952 \index{*recdef|(} |
1953 |
1953 |
1954 Well-founded recursion can express any function whose termination can be |
1954 Well-founded recursion can express any function whose termination can be |
1955 proved by showing that each recursive call makes the argument smaller in a |
1955 proved by showing that each recursive call makes the argument smaller in a |
1956 suitable sense. The recursion need not involve datatypes and there are few |
1956 suitable sense. The recursion need not involve datatypes and there are few |