diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 45613e03af..d05e3dd9e8 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -814,9 +814,12 @@ such that $T$ is an arity of sort $s$. $A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities. \paragraph[Definition]{Definition\index{type of constructor}} -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 -a {\em type of constructor of $I$}. +We say that $T$ is a {\em type of constructor of $I$\index{type of constructor}} +in one of the following two cases: +\begin{itemize} + \item $T$ is $(I~t_1\ldots ~t_n)$ + \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$ +\end{itemize} \paragraph[Examples]{Examples} $\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\ |