COMMENT: question

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.