From 4e8a02a38635cb33ecee78736a2661d169d52046 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 5 Nov 2015 16:18:27 +0100
Subject: COMMENT: question

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

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b3a9925b97..c54481e874 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1373,6 +1373,9 @@ We define now a relation \compat{I:A}{B} between an inductive
 definition $I$ of type $A$ and an arity $B$. This relation states that
 an object in the inductive definition $I$ can be eliminated for
 proving a property $\lb a x \mto P$ of type $B$.
+% QUESTION: Is it necessary to explain the meaning of [I:A|B] in such a complicated way?
+% Couldn't we just say that: "relation [I:A|B] defines which types can we choose as 'result types'
+% with respect to the type of the matched object".
 
 The case of inductive definitions in sorts \Set\ or \Type{} is simple.
 There is no restriction on the sort of the predicate to be
-- 
cgit v1.2.3