diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 16:18:27 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:16 +0100 |
| commit | 4e8a02a38635cb33ecee78736a2661d169d52046 (patch) | |
| tree | 283c44cdff15a80557c1eb1d1247a28f80095e96 /doc/refman/RefMan-cic.tex | |
| parent | 740d35edcb1caf599dfbb956efd0f10aa310b5ae (diff) | |
COMMENT: question
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -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 b3a9925b9..c54481e87 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 |