diff options
| -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". |