diff options
| author | Matej Kosik | 2015-11-05 16:31:57 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:16 +0100 |
| commit | 55fee343ecbb6e510aa9c2729627fe7a758f384b (patch) | |
| tree | 7b0f79aac3559c2705c4f87a223812bd333526d5 | |
| parent | bce5332773276bca755dd47608dd13ae09016ded (diff) | |
CLEANUP: originally, we talked about "B" as an "arity"
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 9cb52dba28..5a8dcfc245 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1372,7 +1372,7 @@ definitions. 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$. +proving a property $\lb a x \mto P$ of arity $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". |