diff options
Diffstat (limited to 'doc')
| -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 eaf400f263..deaa1047c8 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -773,6 +773,9 @@ to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity of sort $s$. (For instance $A\ra \Set$ or $\forall~A:\Prop,A\ra \Prop$ are arities of sort respectively \Set\ and \Prop). \vskip.5em +\noindent A type $T$ is an {\em arity} if there is a $s\in\Sort$ +such that $T$ is an arity of sort $s$. +\vskip.5em \noindent A {\em type of constructor of $I$}\index{Type of constructor} is either a term $(I~t_1\ldots ~t_n)$ or $\fa x:T,C$ with $C$ recursively |