From 6d5a8e69517276d1d13275533aee9fceb42b9d13 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 18:26:59 +0100
Subject: COMMENT: question

---
 doc/refman/RefMan-cic.tex | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc')

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.
-- 
cgit v1.2.3