From fc8e19c82a24fea551b47a99bb68f6f64fc16a01 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 7 Nov 2015 17:30:07 +0100
Subject: COMMENT: question

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 3d56dcac60..8c8537cfb2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1747,6 +1747,8 @@ and $B_{k_i}$
 being an instance of an inductive definition.
 % TODO: We should probably define somewhere explicitely, what we mean by
 %       "x is an instance of an inductive type I".
+%
+% QUESTION: So, $k_i$ is the index of the argument on which $f_i$ is decreasing?
 
 Now in the definition $t_i$, if $f_j$ occurs then it should be applied
 to at least $k_j$ arguments and the $k_j$-th argument should be
-- 
cgit v1.2.3