diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 3cb0b95700..736affe940 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1792,6 +1792,9 @@ The terms structurally smaller than $y$ are: in $g_i$ corresponding to recursive arguments $B_i$ (the ones in which one of the $I_l$ occurs) are structurally smaller than $y$. \end{itemize} +% QUESTION: How could one show, that some of the functions defined below are "guarded" +% in a sense of the definition given above. +% E.g., how could I show that "p" in "plus" below is structurally smaller than "n"? The following definitions are correct, we enter them using the {\tt Fixpoint} command as described in Section~\ref{Fixpoint} and show the internal representation. |