diff options
| author | Matej Kosik | 2015-11-05 16:21:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:16 +0100 |
| commit | d139d73949ee7ab6c070cac98f1af23431967ab0 (patch) | |
| tree | 73bf730fb521a9ddad9b3be64f5ba69df73f3744 | |
| parent | 4e8a02a38635cb33ecee78736a2661d169d52046 (diff) | |
ENH: a forward reference to a place where the concept of "allowed elimination sorts" is actually used
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index c54481e874..49e1649316 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1376,6 +1376,7 @@ 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". +We use this concept to formulate the hypothesis of the typing rule for the match-construct. The case of inductive definitions in sorts \Set\ or \Type{} is simple. There is no restriction on the sort of the predicate to be |